A4:
for x, y being object st x in A & y in A holds

H_{2}(x,y) in A

A5: for x, y being object st x in A & y in A holds

f . (x,y) = H_{2}(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

H

proof

consider f being Function of [:A,A:],A such that
let x, y be object ; :: thesis: ( x in A & y in A implies H_{2}(x,y) in A )

assume ( x in A & y in A ) ; :: thesis: H_{2}(x,y) in A

H_{2}(x,y) in COMPLEX
by XCMPLX_0:def 2;

hence H_{2}(x,y) in A
by A1; :: thesis: verum

end;assume ( x in A & y in A ) ; :: thesis: H

H

hence H

A5: for x, y being object st x in A & y in A holds

f . (x,y) = H

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