defpred S1[ Element of F1(), Element of F2(), Element of F3(), Element of F4()] means $4 = F5($1,$2,$3);
A1:
for x being Element of F1()
for y being Element of F2()
for z being Element of F3() ex t being Element of F4() st S1[x,y,z,t]
;
ex f being Function of [:F1(),F2(),F3():],F4() st
for x being Element of F1()
for y being Element of F2()
for z being Element of F3() holds S1[x,y,z,f . [x,y,z]]
from MULTOP_1:sch 1(A1);
hence
ex f being Function of [:F1(),F2(),F3():],F4() st
for x being Element of F1()
for y being Element of F2()
for z being Element of F3() holds f . [x,y,z] = F5(x,y,z)
; verum