reconsider n = n as non zero natural number by A1;
deffunc H₁( Element of Segm n, Element of Segm n) -> Element of NAT = ($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