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 f ; :: thesis: for a, b, c, d being Element of F1() holds f . (a,b,c,d) = F2(a,b,c,d)
let a, b, c, d be Element of F1(); :: thesis: f . (a,b,c,d) = F2(a,b,c,d)
thus f . (a,b,c,d) = F2(a,b,c,d) by A1; :: thesis: verum