let a, b be non empty set ; :: thesis: ex c being non empty set st
( a /\ c = {} & ex f being Function st
( f is one-to-one & dom f = b & rng f = c ) )
consider d being object such that
A1: for x being set holds not [x,d] in a by Th1;
set C = [:b,{d}:];
consider f being Function such that
A2: ( f is one-to-one & dom f = b & rng f = [:b,{d}:] ) by WELLORD2:def 4, CARD_1:69;
A3: a /\ [:b,{d}:] = {}

proof

assume a /\ [:b,{d}:] <> {} ; :: thesis: contradiction
then consider x being object such that
A5: x in a /\ [:b,{d}:] by XBOOLE_0:def 1;
x in [:b,{d}:] by A5, XBOOLE_0:def 4;
then consider y, z being object such that
A6: ( y in b & z in {d} & x = [y,z] ) by ZFMISC_1:84;
A7: x = [y,d] by A6, TARSKI:def 1;
reconsider y = y as set by A6;
not [y,d] in a by A1;
hence contradiction by A7, A5, XBOOLE_0:def 4; :: thesis: verum

end;

take [:b,{d}:] ; :: thesis: ( a /\ [:b,{d}:] = {} & ex f being Function st
( f is one-to-one & dom f = b & rng f = [:b,{d}:] ) )
thus ( a /\ [:b,{d}:] = {} & ex f being Function st
( f is one-to-one & dom f = b & rng f = [:b,{d}:] ) ) by A3, A2; :: thesis: verum