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