let K, M be Cardinal; :: thesis: for x1, x2 being object st x1 <> x2 holds
( K +` M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K +` M = card ([:K,{x1}:] \/ [:M,{x2}:]) )
let x1, x2 be object ; :: thesis: ( x1 <> x2 implies ( K +` M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K +` M = card ([:K,{x1}:] \/ [:M,{x2}:]) ) )
assume x1 <> x2 ; :: thesis: ( K +` M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K +` M = card ([:K,{x1}:] \/ [:M,{x2}:]) )
then card ([:K,{x1}:] \/ [:M,{x2}:]) = K +` M by Lm1;
hence ( K +` M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K +` M = card ([:K,{x1}:] \/ [:M,{x2}:]) ) by CARD_1:def 2; :: thesis: verum