deffunc H₁( Element of Domains_of T, Element of Domains_of T) -> Element of bool the carrier of T = (Int (Cl ($1 \/ $2))) \/ ($1 \/ $2);
thus for o1, o2 being BinOp of (Domains_of T) st ( for a, b being Element of Domains_of T holds o1 . (a,b) = H₁(a,b) ) & ( for a, b being Element of Domains_of T holds o2 . (a,b) = H₁(a,b) ) holds
o1 = o2 from BINOP_2:sch 2(); :: thesis: verum