let K, M, N be Cardinal; K *` (M +` N) = (K *` M) +` (K *` N)
A1:
[:(card [:K,M:]),{0}:],[:[:K,M:],{0}:] are_equipotent
by Th14;
M,[:M,{0}:] are_equipotent
by Th13;
then A2:
[:K,M:],[:K,[:M,{0}:]:] are_equipotent
by Th15;
[:[:K,M:],{0}:],[:K,M:] are_equipotent
by Th13;
then
[:[:K,M:],{0}:],[:K,[:M,{0}:]:] are_equipotent
by A2, WELLORD2:22;
then A3:
[:(card [:K,M:]),{0}:],[:K,[:M,{0}:]:] are_equipotent
by A1, WELLORD2:22;
A4:
[:(card [:K,N:]),{1}:],[:[:K,N:],{1}:] are_equipotent
by Th14;
[:M,{0}:] misses [:N,{1}:]
by Lm4;
then A5:
[:K,[:M,{0}:]:] misses [:K,[:N,{1}:]:]
by ZFMISC_1:127;
N,[:N,{1}:] are_equipotent
by Th13;
then A6:
[:K,N:],[:K,[:N,{1}:]:] are_equipotent
by Th15;
A7: K *` (M +` N) =
card [:K,(card H3(M,N)):]
by Th17
.=
card [:K,H3(M,N):]
by Th14
.=
card ([:K,[:M,{0}:]:] \/ [:K,[:N,{1}:]:])
by ZFMISC_1:120
;
[:[:K,N:],{1}:],[:K,N:] are_equipotent
by Th13;
then
[:[:K,N:],{1}:],[:K,[:N,{1}:]:] are_equipotent
by A6, WELLORD2:22;
then A8:
[:(card [:K,N:]),{1}:],[:K,[:N,{1}:]:] are_equipotent
by A4, WELLORD2:22;
[:(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:58;
hence K *` (M +` N) =
card ([:(card [:K,M:]),{0}:] \/ [:(card [:K,N:]),{1}:])
by A7, CARD_1:21
.=
(K *` M) +` (K *` N)
by Th17
;
verum