A2: for x being Element of F₁()
for y being Element of F₂() holds F₄(x,y) in the carrier of F₃()

proof

let x be Element of F₁(); :: thesis: for y being Element of F₂() holds F₄(x,y) in the carrier of F₃()
let y be Element of F₂(); :: thesis: F₄(x,y) in the carrier of F₃()
reconsider x1 = x as Element of F₁() ;
reconsider y1 = y as Element of F₂() ;
F₄(x1,y1) is Element of F₃() by A1;
hence F₄(x,y) in the carrier of F₃() ; :: thesis: verum

end;

consider f being Function of [: the carrier of F₁(), the carrier of F₂():], the carrier of F₃() such that
A3: for x being Element of F₁()
for y being Element of F₂() holds f . (x,y) = F₄(x,y) from FUNCT_7:sch 1(A2);
the carrier of [:F₁(),F₂():] = [: the carrier of F₁(), the carrier of F₂():] by Def2;
then reconsider f = f as Function of [:F₁(),F₂():],F₃() ;
take f ; :: thesis: for x being Element of F₁()
for y being Element of F₂() holds f . (x,y) = F₄(x,y)
thus for x being Element of F₁()
for y being Element of F₂() holds f . (x,y) = F₄(x,y) by A3; :: thesis: verum