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 f ; :: thesis: 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)
let a be Element of F₁(); :: thesis: for b being Element of F₂()
for c being Element of F₃() holds f . (a,b,c) = F₅(a,b,c)
let b be Element of F₂(); :: thesis: for c being Element of F₃() holds f . (a,b,c) = F₅(a,b,c)
let c be Element of F₃(); :: thesis: f . (a,b,c) = F₅(a,b,c)
thus f . (a,b,c) = F₅(a,b,c) by A1; :: thesis: verum