deffunc H1( Element of F1(), Element of F1(), Element of F1(), Element of F1()) -> Element of F1() = F2($1,$2,$3,$4);
consider f being Function of [:F1(),F1(),F1(),F1():],F1() such that
A1: for a, b, c, d being Element of F1() holds f . [a,b,c,d] = H1(a,b,c,d) from MULTOP_1:sch 7();
 take o = f; :: thesis: for a, b, c, d being Element of F1() holds o . a,b,c,d = F2(a,b,c,d)
let a, b, c, d be Element of F1(); :: thesis: o . a,b,c,d = F2(a,b,c,d)
thus o . a,b,c,d = F2(a,b,c,d) by A1; :: thesis: verum