deffunc H1( Element of [:F1(),F2():]) -> set = F4(($1 `1 ),($1 `2 ));
A2: for p being Element of [:F1(),F2():] holds H1(p) in F3() by A1;
consider f being Function of [:F1(),F2():],F3() such that
A3: for p being Element of [:F1(),F2():] holds f . p = H1(p) from FUNCT_2:sch 8(A2);
 take f ; :: thesis: for x being Element of F1()
for y being Element of F2() holds f . x,y = F4(x,y)
let x be Element of F1(); :: thesis: for y being Element of F2() holds f . x,y = F4(x,y)
let y be Element of F2(); :: thesis: f . x,y = F4(x,y)
( [x,y] `1 = x & [x,y] `2 = y ) by MCART_1:7;
hence f . x,y = F4(x,y) by A3; :: thesis: verum