consider f being Function of [: the carrier of F1(), the carrier of F2():],F3() such that
A1: for x being Point of F1()
for y being Point of F2() holds f . (x,y) = F4(x,y) from BINOP_1:sch 4();
 [: the carrier of F1(), the carrier of F2():] = the carrier of [:F1(),F2():] by BORSUK_1:def 2;
then reconsider f = f as Function of [:F1(),F2():],F3() ;
take f ; :: thesis: for s being Point of F1()
for t being Point of F2() holds f . (s,t) = F4(s,t)
thus for s being Point of F1()
for t being Point of F2() holds f . (s,t) = F4(s,t) by A1; :: thesis: verum