for f, g being Function of [:A,A:],A st ( for x, y being object st x in A & y in A holds
f . (x,y) = H2(x,y) ) & ( for x, y being object st x in A & y in A holds
g . (x,y) = H2(x,y) ) holds
f = g
from NOMIN_4:sch 3();
hence
for b1, b2 being Function of [:A,A:],A st ( for x, y being object st x in A & y in A holds
b1 . (x,y) = multiplication (x,y) ) & ( for x, y being object st x in A & y in A holds
b2 . (x,y) = multiplication (x,y) ) holds
b1 = b2
; verum