deffunc H₁( Element of REAL n, Element of REAL n) -> Element of REAL n = $1 + $2;
for o1, o2 being BinOp of (REAL n) st ( for a, b being Element of REAL n holds o1 . (a,b) = H₁(a,b) ) & ( for a, b being Element of REAL n holds o2 . (a,b) = H₁(a,b) ) holds
o1 = o2 from BINOP_2:sch 2();
hence for b₁, b₂ being BinOp of (REAL n) st ( for a, b being Element of REAL n holds b₁ . (a,b) = a + b ) & ( for a, b being Element of REAL n holds b₂ . (a,b) = a + b ) holds
b₁ = b₂ ; :: thesis: verum