A4: for x, y being object st x in A & y in A holds
H2(x,y) in A
proof
let x, y be object ; :: thesis: ( x in A & y in A implies H2(x,y) in A )
assume ( x in A & y in A ) ; :: thesis: H2(x,y) in A
H2(x,y) in COMPLEX by XCMPLX_0:def 2;
hence H2(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) = H2(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