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

end;

given a being set , f being Function such that A5: [a,f] in the carrier of S \/ the carrier' of S and
A6: x in rng f ; :: thesis: x in X
consider b being set such that
A7: [b,x] in f by A6, RELAT_1:def 5;
f in proj2 ( the carrier of S \/ the carrier' of S) by A5, 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 A7, TARSKI:def 4;
hence x in X by RELAT_1:def 5; :: thesis: verum