deffunc H₁( VECTOR of V, VECTOR of V) -> VECTOR of V = $1 # $2;
ex B being BinOp of the carrier of V st
for u, v being VECTOR of V holds B . (u,v) = H₁(u,v) from BINOP_1:sch 4();
hence ex b₁ being BinOp of the carrier of V st
for u, v being VECTOR of V holds b₁ . (u,v) = u # v ; :: thesis: verum