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) = {} )

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

assume 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;

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