let K, M, N be Cardinal; (K +` M) +` N = K +` (M +` N)
A1:
card ((K +` M) +` N) = (K +` M) +` N
;
A2:
(K +` M) +` N,[:(K +` M),{0}:] \/ [:N,{2}:] are_equipotent
by Th9;
[:M,{1}:] misses [:N,{2}:]
by Lm4;
then A3:
[:M,{1}:] /\ [:N,{2}:] = {}
;
[:K,{0}:] misses [:N,{2}:]
by Lm4;
then
[:K,{0}:] /\ [:N,{2}:] = {}
;
then ([:K,{0}:] \/ [:M,{1}:]) /\ [:N,{2}:] =
{} \/ {}
by A3, XBOOLE_1:23
.=
{}
;
then A4:
[:K,{0}:] \/ [:M,{1}:] misses [:N,{2}:]
;
( K +` M,[:K,{0}:] \/ [:M,{1}:] are_equipotent & K +` M,[:(K +` M),{0}:] are_equipotent )
by CARD_1:69, Th9;
then A5:
[:(K +` M),{0}:],[:K,{0}:] \/ [:M,{1}:] are_equipotent
by WELLORD2:15;
[:K,{0}:] misses [:N,{2}:]
by Lm4;
then A6:
[:K,{0}:] /\ [:N,{2}:] = {}
;
[:K,{0}:] misses [:M,{1}:]
by Lm4;
then
[:K,{0}:] /\ [:M,{1}:] = {}
;
then [:K,{0}:] /\ ([:M,{1}:] \/ [:N,{2}:]) =
{} \/ {}
by A6, XBOOLE_1:23
.=
{}
;
then A7:
[:K,{0}:] misses [:M,{1}:] \/ [:N,{2}:]
;
( M +` N,[:M,{1}:] \/ [:N,{2}:] are_equipotent & M +` N,[:(M +` N),{2}:] are_equipotent )
by CARD_1:69, Th9;
then A8:
[:(M +` N),{2}:],[:M,{1}:] \/ [:N,{2}:] are_equipotent
by WELLORD2:15;
[:K,{0}:] misses [:(M +` N),{2}:]
by Lm4;
then A9:
[:K,{0}:] \/ ([:M,{1}:] \/ [:N,{2}:]),[:K,{0}:] \/ [:(M +` N),{2}:] are_equipotent
by A7, A8, CARD_1:31;
[:(K +` M),{0}:] misses [:N,{2}:]
by Lm4;
then A10:
[:(K +` M),{0}:] \/ [:N,{2}:],([:K,{0}:] \/ [:M,{1}:]) \/ [:N,{2}:] are_equipotent
by A4, A5, CARD_1:31;
[:K,{0}:] \/ ([:M,{1}:] \/ [:N,{2}:]) = ([:K,{0}:] \/ [:M,{1}:]) \/ [:N,{2}:]
by XBOOLE_1:4;
then
[:(K +` M),{0}:] \/ [:N,{2}:],[:K,{0}:] \/ [:(M +` N),{2}:] are_equipotent
by A10, A9, WELLORD2:15;
then A11:
(K +` M) +` N,[:K,{0}:] \/ [:(M +` N),{2}:] are_equipotent
by A2, WELLORD2:15;
[:K,{0}:] \/ [:(M +` N),{2}:],K +` (M +` N) are_equipotent
by Th9;
then
(K +` M) +` N,K +` (M +` N) are_equipotent
by A11, WELLORD2:15;
hence
(K +` M) +` N = K +` (M +` N)
by A1, CARD_1:def 2; verum