defpred S1[ Element of F1(), Element of F1(), Element of F1(), Element of F1()] means for r being Element of F1() st r = $4 holds
P1[$1,$2,$3,r];
A2:
for x, y, z being Element of F1() ex t being Element of F1() st S1[x,y,z,t]
proof
let x,
y,
z be
Element of
F1();
ex t being Element of F1() st S1[x,y,z,t]
consider t being
Element of
F1()
such that A3:
P1[
x,
y,
z,
t]
by A1;
take
t
;
S1[x,y,z,t]
thus
S1[
x,
y,
z,
t]
by A3;
verum
end;
consider f being Function of [:F1(),F1(),F1():],F1() such that
A4:
for a, b, c being Element of F1() holds S1[a,b,c,f . [a,b,c]]
from MULTOP_1:sch 1(A2);
take
f
; for a, b, c being Element of F1() holds P1[a,b,c,f . (a,b,c)]
let a, b, c be Element of F1(); P1[a,b,c,f . (a,b,c)]
thus
P1[a,b,c,f . (a,b,c)]
by A4; verum