set A = StoneS L;
deffunc H₁( Element of StoneS L, Element of StoneS L) -> Element of StoneS L = $1 /\ $2;
thus for o1, o2 being BinOp of (StoneS L) st ( for a, b being Element of StoneS L holds o1 . (a,b) = H₁(a,b) ) & ( for a, b being Element of StoneS L holds o2 . (a,b) = H₁(a,b) ) holds
o1 = o2 from BINOP_2:sch 2(); :: thesis: verum