consider f being Function of [: the carrier of F_{1}(), the carrier of F_{2}():],F_{3}() such that

A1: for x being Point of F_{1}()

for y being Point of F_{2}() holds f . (x,y) = F_{4}(x,y)
from BINOP_1:sch 4();

[: the carrier of F_{1}(), the carrier of F_{2}():] = the carrier of [:F_{1}(),F_{2}():]
by BORSUK_1:def 2;

then reconsider f = f as Function of [:F_{1}(),F_{2}():],F_{3}() ;

take f ; :: thesis: for s being Point of F_{1}()

for t being Point of F_{2}() holds f . (s,t) = F_{4}(s,t)

thus for s being Point of F_{1}()

for t being Point of F_{2}() holds f . (s,t) = F_{4}(s,t)
by A1; :: thesis: verum

A1: for x being Point of F

for y being Point of F

[: the carrier of F

then reconsider f = f as Function of [:F

take f ; :: thesis: for s being Point of F

for t being Point of F

thus for s being Point of F

for t being Point of F