deffunc H₁( Element of NATPLUS , Element of NATPLUS ) -> Element of NAT = $1 lcm $2;
thus for o1, o2 being BinOp of NATPLUS st ( for a, b being Element of NATPLUS holds o1 . a,b = H₁(a,b) ) & ( for a, b being Element of NATPLUS holds o2 . a,b = H₁(a,b) ) holds
o1 = o2 from BINOP_2:sch 2(); :: thesis: verum