reconsider n = n as non zero Nat by A1, TARSKI:1;

deffunc H_{1}( 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_{1}(a) ) & ( for a being Element of Segm n holds f2 . a = H_{1}(a) ) holds

f1 = f2 from LMOD_7:sch 2();

hence for b_{1}, b_{2} being UnOp of (Segm n) st ( for k being Element of Segm n holds b_{1} . k = (n - k) mod n ) & ( for k being Element of Segm n holds b_{2} . k = (n - k) mod n ) holds

b_{1} = b_{2}
; :: thesis: verum

deffunc H

for f1, f2 being UnOp of (Segm n) st ( for a being Element of Segm n holds f1 . a = H

f1 = f2 from LMOD_7:sch 2();

hence for b

b