defpred S₁[ Element of F₁(), Element of F₁(), Element of F₁(), Element of F₁(), Element of F₁()] means for r being Element of F₁() st r = $5 holds
P₁[$1,$2,$3,$4,$5];
A2: for x, y, z, s being Element of F₁() ex t being Element of F₁() st S₁[x,y,z,s,t]

proof

let x, y, z, s be Element of F₁(); :: thesis: ex t being Element of F₁() st S₁[x,y,z,s,t]
consider t being Element of F₁() such that
A3: P₁[x,y,z,s,t] by A1;
take t ; :: thesis: S₁[x,y,z,s,t]
thus S₁[x,y,z,s,t] by A3; :: thesis: verum

end;

consider f being Function of [:F₁(),F₁(),F₁(),F₁():],F₁() such that
A4: for a, b, c, d being Element of F₁() holds S₁[a,b,c,d,f . [a,b,c,d]] from MULTOP_1:sch 5(A2);
take o = f; :: thesis: for a, b, c, d being Element of F₁() holds P₁[a,b,c,d,o . a,b,c,d]
let a, b, c, d be Element of F₁(); :: thesis: P₁[a,b,c,d,o . a,b,c,d]
thus P₁[a,b,c,d,o . a,b,c,d] by A4; :: thesis: verum