defpred S₁[ object , object ] means ( $2 in the carrier of F₁() & P₁[$1,$2] );
A2: for S being object st S in F₂() holds
ex x being object st
( x in the carrier of F₁() & S₁[S,x] )

proof

let S be object ; :: thesis: ( S in F₂() implies ex x being object st
( x in the carrier of F₁() & S₁[S,x] ) )
assume A3: S in F₂() ; :: thesis: ex x being object st
( x in the carrier of F₁() & S₁[S,x] )
then reconsider Q = S as Subset of F₁() ;
consider x being Point of F₁() such that
A4: P₁[Q,x] by A1, A3;
take x ; :: thesis: ( x in the carrier of F₁() & S₁[S,x] )
thus ( x in the carrier of F₁() & S₁[S,x] ) by A4; :: thesis: verum

end;

consider f being Function such that
A5: dom f = F₂() and
A6: rng f c= the carrier of F₁() and
A7: for S being object st S in F₂() holds
S₁[S,f . S] from FUNCT_1:sch 6(A2);
reconsider f = f as Function of F₂(), the carrier of F₁() by A5, A6, FUNCT_2:def 1, RELSET_1:4;
take f ; :: thesis: for S being Subset of F₁() st S in F₂() holds
P₁[S,f . S]
thus for S being Subset of F₁() st S in F₂() holds
P₁[S,f . S] by A7; :: thesis: verum