let a, b be Aleph; :: thesis: ( a c= b implies exp a,b = exp 2,b )
assume A1: a c= b ; :: thesis: exp a,b = exp 2,b
( b c= b & 2 in a & card 2 <> card 0 & a <> 0 & card 0 = 0 & card 2 = 2 ) by Lm1, Th25;
then A2: exp 2,b c= exp a,b by CARD_3:138;
( card a = a & card a in card (bool a) & card (bool a) = exp 2,(card a) ) by CARD_1:30, CARD_1:def 5, CARD_2:44;
then ( exp a,b c= exp (exp 2,a),b & exp (exp 2,a),b = exp 2,(a *` b) & a *` b = b ) by A1, Th27, CARD_2:43, CARD_3:138;
hence exp a,b = exp 2,b by A2, XBOOLE_0:def 10; :: thesis: verum