deffunc H₁( Element of StoneS L, Element of StoneS L) -> Element of StoneS L = $1 \/ $2;
thus ex F being BinOp of (StoneS L) st
for P, Q being Element of StoneS L holds F . (P,Q) = H₁(P,Q) from BINOP_1:sch 4(); :: thesis: verum