defpred S₁[ Element of F₁(), Element of F₂(), Element of F₃(), Element of F₄(), Element of F₅()] means $5 = F₆($1,$2,$3,$4);
A1: for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃()
for s being Element of F₄() ex t being Element of F₅() st S₁[x,y,z,s,t] ;
ex f being Function of [:F₁(),F₂(),F₃(),F₄():],F₅() st
for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃()
for s being Element of F₄() holds S₁[x,y,z,s,f . [x,y,z,s]] from MULTOP_1:sch 5(A1);
hence ex f being Function of [:F₁(),F₂(),F₃(),F₄():],F₅() st
for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃()
for s being Element of F₄() holds f . [x,y,z,s] = F₆(x,y,z,s) ; :: thesis: verum