let K, M, N be Cardinal; exp (K,(M *` N)) = exp ((exp (K,M)),N)
A1:
Funcs (M,K), card (Funcs (M,K)) are_equipotent
by CARD_1:def 5;
( [:M,N:],M *` N are_equipotent & [:N,M:],[:M,N:] are_equipotent )
by Lm2, CARD_1:def 5;
then
[:N,M:],M *` N are_equipotent
by WELLORD2:22;
hence exp (K,(M *` N)) =
card (Funcs ([:N,M:],K))
by FUNCT_5:67
.=
card (Funcs (N,(Funcs (M,K))))
by FUNCT_5:70
.=
exp ((exp (K,M)),N)
by A1, FUNCT_5:67
;
verum