A4:
for x, y being object st x in A & y in A holds
H2(x,y) in A
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
; 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; verum