A2: for x being Element of F1()
for y being Element of F2() holds F4(x,y) in the carrier of F3()
proof
let x be Element of F1(); :: thesis: for y being Element of F2() holds F4(x,y) in the carrier of F3()
let y be Element of F2(); :: thesis: F4(x,y) in the carrier of F3()
reconsider x1 = x as Element of F1() ;
reconsider y1 = y as Element of F2() ;
F4(x1,y1) is Element of F3() by A1;
hence F4(x,y) in the carrier of F3() ; :: thesis: verum
end;
consider f being Function of [: the carrier of F1(), the carrier of F2():], the carrier of F3() such that
A3: for x being Element of F1()
for y being Element of F2() holds f . (x,y) = F4(x,y) from FUNCT_7:sch 1(A2);
 the carrier of [:F1(),F2():] = [: the carrier of F1(), the carrier of F2():] by Def2;
then reconsider f = f as Function of [:F1(),F2():],F3() ;
take f ; :: thesis: for x being Element of F1()
for y being Element of F2() holds f . (x,y) = F4(x,y)
thus for x being Element of F1()
for y being Element of F2() holds f . (x,y) = F4(x,y) by A3; :: thesis: verum