let x, y be object ; for X, Y being set st x <> y holds
(card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:])
let X, Y be set ; ( x <> y implies (card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:]) )
assume A1:
x <> y
; (card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:])
( X, card X are_equipotent & Y, card Y are_equipotent )
by CARD_1:def 2;
then
card H4(X,Y,x,y) = card H4( card X, card Y,x,y)
by A1, Th11;
hence
(card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:])
by A1, Lm1; verum