deffunc H₁( Element of [:F₁(),F₂():]) -> set = F₄(($1 `1),($1 `2));
A2: for p being Element of [:F₁(),F₂():] holds H₁(p) in F₃() by A1;
consider f being Function of [:F₁(),F₂():],F₃() such that
A3: for p being Element of [:F₁(),F₂():] holds f . p = H₁(p) from FUNCT_2:sch 8(A2);
take f ; :: thesis: for x being Element of F₁()
for y being Element of F₂() holds f . (x,y) = F₄(x,y)
let x be Element of F₁(); :: thesis: for y being Element of F₂() holds f . (x,y) = F₄(x,y)
let y be Element of F₂(); :: thesis: f . (x,y) = F₄(x,y)
( [x,y] `1 = x & [x,y] `2 = y ) ;
hence f . (x,y) = F₄(x,y) by A3; :: thesis: verum