defpred S1[ object , object ] means ( $2 in the carrier of F1() & P1[$1,$2] );
A2:
for S being object st S in F2() holds
ex x being object st
( x in the carrier of F1() & S1[S,x] )
proof
let S be
object ;
( S in F2() implies ex x being object st
( x in the carrier of F1() & S1[S,x] ) )
assume A3:
S in F2()
;
ex x being object st
( x in the carrier of F1() & S1[S,x] )
then reconsider Q =
S as
Subset of
F1() ;
consider x being
Point of
F1()
such that A4:
P1[
Q,
x]
by A1, A3;
take
x
;
( x in the carrier of F1() & S1[S,x] )
thus
(
x in the
carrier of
F1() &
S1[
S,
x] )
by A4;
verum
end;
consider f being Function such that
A5:
dom f = F2()
and
A6:
rng f c= the carrier of F1()
and
A7:
for S being object st S in F2() holds
S1[S,f . S]
from FUNCT_1:sch 6(A2);
reconsider f = f as Function of F2(), the carrier of F1() by A5, A6, FUNCT_2:def 1, RELSET_1:4;
take
f
; for S being Subset of F1() st S in F2() holds
P1[S,f . S]
thus
for S being Subset of F1() st S in F2() holds
P1[S,f . S]
by A7; verum