A2: for x, y being object st x in A & y in A holds
H₁(x,y) in A

proof

let x, y be object ; :: thesis: ( x in A & y in A implies H₁(x,y) in A )
assume ( x in A & y in A ) ; :: thesis: H₁(x,y) in A
H₁(x,y) in COMPLEX by XCMPLX_0:def 2;
hence H₁(x,y) in A by A1; :: thesis: verum

end;

consider f being Function of [:A,A:],A such that
A3: for x, y being object st x in A & y in A holds
f . (x,y) = H₁(x,y) from BINOP_1:sch 2(A2);
take f ; :: thesis: for x, y being object st x in A & y in A holds
f . (x,y) = addition (x,y)
thus for x, y being object st x in A & y in A holds
f . (x,y) = addition (x,y) by A3; :: thesis: verum