reconsider n = n as natural non zero Number by A1;
deffunc H₁( Element of Segm n, Element of Segm n) -> set = ($1 * $2) mod n;
for o1, o2 being BinOp of (Segm n) st ( for a, b being Element of Segm n holds o1 . (a,b) = H₁(a,b) ) & ( for a, b being Element of Segm n holds o2 . (a,b) = H₁(a,b) ) holds
o1 = o2 from BINOP_2:sch 2();
hence for b₁, b₂ being BinOp of (Segm n) st ( for k, l being Element of Segm n holds b₁ . (k,l) = (k * l) mod n ) & ( for k, l being Element of Segm n holds b₂ . (k,l) = (k * l) mod n ) holds
b₁ = b₂ ; :: thesis: verum