consider Y being set such that

A: ( card (Z \/ X) c= card Y & (Z \/ X) /\ Y = {} ) by thre;

card X c= card (Z \/ X) by XBOOLE_1:7, CARD_1:11;

then card X c= card Y by A;

then consider f being Function such that

B: ( f is one-to-one & dom f = X & rng f c= Y ) by CARD_1:10;

take f ; :: thesis: ( dom f = X & f is one-to-one & (rng f) /\ (X \/ Z) = {} )

A: ( card (Z \/ X) c= card Y & (Z \/ X) /\ Y = {} ) by thre;

card X c= card (Z \/ X) by XBOOLE_1:7, CARD_1:11;

then card X c= card Y by A;

then consider f being Function such that

B: ( f is one-to-one & dom f = X & rng f c= Y ) by CARD_1:10;

take f ; :: thesis: ( dom f = X & f is one-to-one & (rng f) /\ (X \/ Z) = {} )

now :: thesis: not (rng f) /\ (X \/ Z) <> {}

hence
( dom f = X & f is one-to-one & (rng f) /\ (X \/ Z) = {} )
by B; :: thesis: verumassume C:
(rng f) /\ (X \/ Z) <> {}
; :: thesis: contradiction

set o = the Element of (rng f) /\ (X \/ Z);

( the Element of (rng f) /\ (X \/ Z) in rng f & the Element of (rng f) /\ (X \/ Z) in X \/ Z ) by C, XBOOLE_0:def 4;

hence contradiction by A, B, XBOOLE_0:def 4; :: thesis: verum

end;set o = the Element of (rng f) /\ (X \/ Z);

( the Element of (rng f) /\ (X \/ Z) in rng f & the Element of (rng f) /\ (X \/ Z) in X \/ Z ) by C, XBOOLE_0:def 4;

hence contradiction by A, B, XBOOLE_0:def 4; :: thesis: verum