theorem Th9: :: CARD_2:10

for K, M being Cardinal
for x1, x2 being object st x1 <> x2 holds
( K +` M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K +` M = card ([:K,{x1}:] \/ [:M,{x2}:]) )