reconsider n = n as non zero Nat by A1, TARSKI:1;
deffunc H₁( Element of Segm n) -> object = (n - $1) mod n;
for f1, f2 being UnOp of (Segm n) st ( for a being Element of Segm n holds f1 . a = H₁(a) ) & ( for a being Element of Segm n holds f2 . a = H₁(a) ) holds
f1 = f2 from LMOD_7:sch 2();
hence for b₁, b₂ being UnOp of (Segm n) st ( for k being Element of Segm n holds b₁ . k = (n - k) mod n ) & ( for k being Element of Segm n holds b₂ . k = (n - k) mod n ) holds
b₁ = b₂ ; :: thesis: verum