defpred S1[ object , object ] means $2 = F3((In ($1,F1())));
A2:
for x being Element of F1() ex y being Element of F2() st S1[x,y]
proof
let x be
Element of
F1();
ex y being Element of F2() st S1[x,y]
reconsider y =
F3(
x) as
Element of
F2()
by A1;
take
y
;
S1[x,y]
thus
S1[
x,
y]
;
verum
end;
consider f being Function of F1(),F2() such that
A3:
for x being Element of F1() holds S1[x,f . x]
from FUNCT_2:sch 3(A2);
take
f
; for x being Element of F1() holds f . x = F3(x)
let x be Element of F1(); f . x = F3(x)
In (x,F1()) = x
;
hence
f . x = F3(x)
by A3; verum