set A = the carrier of S \/ the carrier' of S;
take X = proj2 (union (proj2 ( the carrier of S \/ the carrier' of S))); :: thesis: for x being object holds
( x in X iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) )
let x be object ; :: thesis: ( x in X iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) )

hereby :: thesis: ( ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) implies x in X )

assume x in X ; :: thesis: ex c being set ex b being Function st
( [c,b] in the carrier of S \/ the carrier' of S & x in rng b )
then consider a being object such that
A2: [a,x] in union (proj2 ( the carrier of S \/ the carrier' of S)) by XTUPLE_0:def 13;
consider b being set such that
A3: [a,x] in b and
A4: b in proj2 ( the carrier of S \/ the carrier' of S) by A2, TARSKI:def 4;
reconsider b = b as Function by A4, A1;
b in proj2 ( the carrier of S \/ the carrier' of S) by A4;
then consider c being object such that
A5: [c,b] in the carrier of S \/ the carrier' of S by XTUPLE_0:def 13;
reconsider c = c as set by TARSKI:1;
take c = c; :: thesis: ex b being Function st
( [c,b] in the carrier of S \/ the carrier' of S & x in rng b )
take b = b; :: thesis: ( [c,b] in the carrier of S \/ the carrier' of S & x in rng b )
thus ( [c,b] in the carrier of S \/ the carrier' of S & x in rng b ) by A3, A5, XTUPLE_0:def 13; :: thesis: verum

end;

given a being set , f being Function such that A6: [a,f] in the carrier of S \/ the carrier' of S and
A7: x in rng f ; :: thesis: x in X
consider b being object such that
A8: [b,x] in f by A7, XTUPLE_0:def 13;
f in proj2 ( the carrier of S \/ the carrier' of S) by A6, XTUPLE_0:def 13;
then f in proj2 ( the carrier of S \/ the carrier' of S) ;
then [b,x] in union (proj2 ( the carrier of S \/ the carrier' of S)) by A8, TARSKI:def 4;
hence x in X by XTUPLE_0:def 13; :: thesis: verum