set A = Topology_of T;

deffunc H_{1}( Element of Topology_of T, Element of Topology_of T) -> Element of Topology_of T = $1 \/ $2;

thus for o1, o2 being BinOp of (Topology_of T) st ( for a, b being Element of Topology_of T holds o1 . (a,b) = H_{1}(a,b) ) & ( for a, b being Element of Topology_of T holds o2 . (a,b) = H_{1}(a,b) ) holds

o1 = o2 from BINOP_2:sch 2(); :: thesis: verum

deffunc H

thus for o1, o2 being BinOp of (Topology_of T) st ( for a, b being Element of Topology_of T holds o1 . (a,b) = H

o1 = o2 from BINOP_2:sch 2(); :: thesis: verum