deffunc H1( VECTOR of V, VECTOR of V) -> VECTOR of V = $1 # $2;
for o1, o2 being BinOp of the carrier of V st ( for a, b being Element of V holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of V holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2
from BINOP_2:sch 2();
hence
for b1, b2 being BinOp of the carrier of V st ( for u, v being VECTOR of V holds b1 . (u,v) = u # v ) & ( for u, v being VECTOR of V holds b2 . (u,v) = u # v ) holds
b1 = b2
; verum