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