defpred S1[ object , object ] means $2 = F2($1);
A1:
for x being object st x in F1() holds
ex y being object st S1[x,y]
;
A2:
for x, y1, y2 being object st x in F1() & S1[x,y1] & S1[x,y2] holds
y1 = y2
;
consider f being Function such that
A3:
dom f = F1()
and
A4:
for x being object st x in F1() holds
S1[x,f . x]
from FUNCT_1:sch 2(A2, A1);
take
f
; ( dom f = F1() & ( for X being set st X in F1() holds
f . X = F2(X) ) )
thus
dom f = F1()
by A3; for X being set st X in F1() holds
f . X = F2(X)
thus
for X being set st X in F1() holds
f . X = F2(X)
by A4; verum