consider f being Function of [:F₁(),F₂(),F₃():],F₄() such that
A1: for a being Element of F₁()
for b being Element of F₂()
for c being Element of F₃() holds f . [a,b,c] = F₅(a,b,c) from MULTOP_1:sch 3();
take o = f; :: thesis: for a being Element of F₁()
for b being Element of F₂()
for c being Element of F₃() holds o . a,b,c = F₅(a,b,c)
let a be Element of F₁(); :: thesis: for b being Element of F₂()
for c being Element of F₃() holds o . a,b,c = F₅(a,b,c)
let b be Element of F₂(); :: thesis: for c being Element of F₃() holds o . a,b,c = F₅(a,b,c)
let c be Element of F₃(); :: thesis: o . a,b,c = F₅(a,b,c)
thus o . a,b,c = F₅(a,b,c) by A1; :: thesis: verum