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) = H_{1}(x,y) ) & ( for x, y being object st x in A & y in A holds

g . (x,y) = H_{1}(x,y) ) holds

f = g from NOMIN_4:sch 3();

hence for b_{1}, b_{2} being Function of [:A,A:],A st ( for x, y being object st x in A & y in A holds

b_{1} . (x,y) = addition (x,y) ) & ( for x, y being object st x in A & y in A holds

b_{2} . (x,y) = addition (x,y) ) holds

b_{1} = b_{2}
; :: thesis: verum

f . (x,y) = H

g . (x,y) = H

f = g from NOMIN_4:sch 3();

hence for b

b

b

b