set A = the carrier of S \/ the carrier' of S;
take X = proj2 (union (SubFuncs (proj2 (the carrier of S \/ the carrier' of S)))); :: thesis: for x being set 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 set ; :: 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 set such that
A1: [a,x] in union (SubFuncs (proj2 (the carrier of S \/ the carrier' of S))) by RELAT_1:def 5;
consider b being set such that
A2: ( [a,x] in b & b in SubFuncs (proj2 (the carrier of S \/ the carrier' of S)) ) by A1, TARSKI:def 4;
reconsider b = b as Function by A2, FUNCT_6:def 1;
b in proj2 (the carrier of S \/ the carrier' of S) by A2, FUNCT_6:def 1;
then consider c being set such that
A3: [c,b] in the carrier of S \/ the carrier' of S by RELAT_1:def 5;
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 A2, A3, RELAT_1:def 5; :: thesis: verum

end;

given a being set , f being Function such that A4: ( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ; :: thesis: x in X
consider b being set such that
A5: [b,x] in f by A4, RELAT_1:def 5;
f in proj2 (the carrier of S \/ the carrier' of S) by A4, RELAT_1:def 5;
then f in SubFuncs (proj2 (the carrier of S \/ the carrier' of S)) by FUNCT_6:def 1;
then [b,x] in union (SubFuncs (proj2 (the carrier of S \/ the carrier' of S))) by A5, TARSKI:def 4;
hence x in X by RELAT_1:def 5; :: thesis: verum