• On cherche * tel que * m n = m*n

• On a :

m*n ≡ s^m*n 0 ≡ sⁿ (sⁿ (…(sⁿ 0)..))

       = n s (n s ( … (n s 0)..)) = m (n s) 0

• On veut donc :   

         * m n = m (n s) 0 = C m 0 (n s) = C C 0 m (n s)

= B (C C 0 m) n s = C (B (C C 0 m)) s n

= C C s (B (C C 0 m)) n = B (C C s) B (C C 0 m) n

= B (B (C C s) B) (C C 0) m n

• On peut donc prendre : 
                      * ≡_def B (B (C C s) B) (C C 0)