thus ex B being BinOp of (V .. W) st
for S1, S2 being Element of V .. W holds B . (S1,S2) = H₂(S1,S2) from BINOP_1:sch 4(); :: thesis: verum