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 2;
( [:M,N:],M *` N are_equipotent & [:N,M:],[:M,N:] are_equipotent )
by Lm2, CARD_1:def 2;
then
[:N,M:],M *` N are_equipotent
by WELLORD2:15;
hence exp (K,(M *` N)) =
card (Funcs ([:N,M:],K))
by FUNCT_5:60
.=
card (Funcs (N,(Funcs (M,K))))
by FUNCT_5:63
.=
exp ((exp (K,M)),N)
by A1, FUNCT_5:60
;
verum