A4: 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
A5: for x, y being object st x in A & y in A holds
f . (x,y) = H₂(x,y) from BINOP_1:sch 2(A4);
take f ; :: thesis: for x, y being object st x in A & y in A holds
f . (x,y) = multiplication (x,y)
thus for x, y being object st x in A & y in A holds
f . (x,y) = multiplication (x,y) by A5; :: thesis: verum