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₁(x,y) ) & ( for x, y being object st x in A & y in A holds
g . (x,y) = H₁(x,y) ) holds
f = g from NOMIN_4:sch 3();
hence for b₁, b₂ being Function of [:A,A:],A st ( for x, y being object st x in A & y in A holds
b₁ . (x,y) = addition (x,y) ) & ( for x, y being object st x in A & y in A holds
b₂ . (x,y) = addition (x,y) ) holds
b₁ = b₂ ; :: thesis: verum