let K, M, N be Cardinal; :: thesis: (K +` M) +` N = K +` (M +` N)
A1: ( (K +` M) +` N,[:(K +` M),{0 }:] \/ [:N,{2}:] are_equipotent & K +` M,[:K,{0 }:] \/ [:M,{1}:] are_equipotent & K +` (M +` N),[:K,{0 }:] \/ [:(M +` N),{2}:] are_equipotent & M +` N,[:M,{1}:] \/ [:N,{2}:] are_equipotent & K +` M,[:(K +` M),{0 }:] are_equipotent & M +` N,[:(M +` N),{2}:] are_equipotent ) by Th13, Th17;
A2: [:(K +` M),{0 }:] misses [:N,{2}:] by Lm4;
( [:K,{0 }:] misses [:N,{2}:] & [:M,{1}:] misses [:N,{2}:] ) by Lm4;
then ( [:K,{0 }:] /\ [:N,{2}:] = {} & [:M,{1}:] /\ [:N,{2}:] = {} ) by XBOOLE_0:def 7;
then ([:K,{0 }:] \/ [:M,{1}:]) /\ [:N,{2}:] = {} \/ {} by XBOOLE_1:23
.= {} ;
then A3: [:K,{0 }:] \/ [:M,{1}:] misses [:N,{2}:] by XBOOLE_0:def 7;
( [:(K +` M),{0 }:],[:K,{0 }:] \/ [:M,{1}:] are_equipotent & [:N,{2}:],[:N,{2}:] are_equipotent ) by A1, WELLORD2:22;
then A4: [:(K +` M),{0 }:] \/ [:N,{2}:],([:K,{0 }:] \/ [:M,{1}:]) \/ [:N,{2}:] are_equipotent by A2, A3, CARD_1:58;
A5: [:K,{0 }:] misses [:(M +` N),{2}:] by Lm4;
( [:K,{0 }:] misses [:M,{1}:] & [:K,{0 }:] misses [:N,{2}:] ) by Lm4;
then ( [:K,{0 }:] /\ [:M,{1}:] = {} & [:K,{0 }:] /\ [:N,{2}:] = {} ) by XBOOLE_0:def 7;
then [:K,{0 }:] /\ ([:M,{1}:] \/ [:N,{2}:]) = {} \/ {} by XBOOLE_1:23
.= {} ;
then A6: [:K,{0 }:] misses [:M,{1}:] \/ [:N,{2}:] by XBOOLE_0:def 7;
( [:(M +` N),{2}:],[:M,{1}:] \/ [:N,{2}:] are_equipotent & [:K,{0 }:],[:K,{0 }:] are_equipotent ) by A1, WELLORD2:22;
then ( [:K,{0 }:] \/ ([:M,{1}:] \/ [:N,{2}:]),[:K,{0 }:] \/ [:(M +` N),{2}:] are_equipotent & [:K,{0 }:] \/ ([:M,{1}:] \/ [:N,{2}:]) = ([:K,{0 }:] \/ [:M,{1}:]) \/ [:N,{2}:] ) by A5, A6, CARD_1:58, XBOOLE_1:4;
then [:(K +` M),{0 }:] \/ [:N,{2}:],[:K,{0 }:] \/ [:(M +` N),{2}:] are_equipotent by A4, WELLORD2:22;
then ( (K +` M) +` N,[:K,{0 }:] \/ [:(M +` N),{2}:] are_equipotent & [:K,{0 }:] \/ [:(M +` N),{2}:],K +` (M +` N) are_equipotent ) by A1, WELLORD2:22;
then ( (K +` M) +` N,K +` (M +` N) are_equipotent & card ((K +` M) +` N) = (K +` M) +` N ) by WELLORD2:22;
hence (K +` M) +` N = K +` (M +` N) by CARD_1:def 5; :: thesis: verum