deffunc H_{1}( 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_{1}(a,b) ) & ( for a, b being Element of REAL n holds o2 . (a,b) = H_{1}(a,b) ) holds

o1 = o2 from BINOP_2:sch 2();

hence for b_{1}, b_{2} being BinOp of (REAL n) st ( for a, b being Element of REAL n holds b_{1} . (a,b) = a + b ) & ( for a, b being Element of REAL n holds b_{2} . (a,b) = a + b ) holds

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

for o1, o2 being BinOp of (REAL n) st ( for a, b being Element of REAL n holds o1 . (a,b) = H

o1 = o2 from BINOP_2:sch 2();

hence for b

b