let K, M, N be Cardinal; K *` (M +` N) = (K *` M) +` (K *` N)
A1:
[:(card [:K,M:]),{0}:],[:[:K,M:],{0}:] are_equipotent
by Th6;
M,[:M,{0}:] are_equipotent
by CARD_1:69;
then A2:
[:K,M:],[:K,[:M,{0}:]:] are_equipotent
by Th7;
[:[:K,M:],{0}:],[:K,M:] are_equipotent
by CARD_1:69;
then
[:[:K,M:],{0}:],[:K,[:M,{0}:]:] are_equipotent
by A2, WELLORD2:15;
then A3:
[:(card [:K,M:]),{0}:],[:K,[:M,{0}:]:] are_equipotent
by A1, WELLORD2:15;
A4:
[:(card [:K,N:]),{1}:],[:[:K,N:],{1}:] are_equipotent
by Th6;
[:M,{0}:] misses [:N,{1}:]
by Lm4;
then A5:
[:K,[:M,{0}:]:] misses [:K,[:N,{1}:]:]
by ZFMISC_1:104;
N,[:N,{1}:] are_equipotent
by CARD_1:69;
then A6:
[:K,N:],[:K,[:N,{1}:]:] are_equipotent
by Th7;
A7: K *` (M +` N) =
card [:K,(card H3(M,N)):]
by Th9
.=
card [:K,H3(M,N):]
by Th6
.=
card ([:K,[:M,{0}:]:] \/ [:K,[:N,{1}:]:])
by ZFMISC_1:97
;
[:[:K,N:],{1}:],[:K,N:] are_equipotent
by CARD_1:69;
then
[:[:K,N:],{1}:],[:K,[:N,{1}:]:] are_equipotent
by A6, WELLORD2:15;
then A8:
[:(card [:K,N:]),{1}:],[:K,[:N,{1}:]:] are_equipotent
by A4, WELLORD2:15;
[:(card [:K,M:]),{0}:] misses [:(card [:K,N:]),{1}:]
by Lm4;
then
[:(card [:K,M:]),{0}:] \/ [:(card [:K,N:]),{1}:],[:K,[:M,{0}:]:] \/ [:K,[:N,{1}:]:] are_equipotent
by A3, A8, A5, CARD_1:31;
hence K *` (M +` N) =
card ([:(card [:K,M:]),{0}:] \/ [:(card [:K,N:]),{1}:])
by A7, CARD_1:5
.=
(K *` M) +` (K *` N)
by Th9
;
verum