defpred S1[ object , object ] means $2 = F3($1); A2:
for x being object st x in F1() holds ex y being object st ( y in F2() & S1[x,y] )
byA1;
ex f being Function of F1(),F2() st for x being object st x in F1() holds S1[x,f . x]
fromFUNCT_2:sch 1(A2); then consider f being Function of F1(),F2() such that A3:
for x being object st x in F1() holds f . x = F3(x)
;
for x being Element of F1() holds f . x = F3(x)
byA3; hence
ex f being Function of F1(),F2() st for x being Element of F1() holds f . x = F3(x)
; :: thesis: verum