reconsider n = n as non zero Nat by A1, TARSKI:1;
set f = { [k,((n - k) mod n)] where k is Element of NAT : k < n } ;
A2:
for x being object st x in { [k,((n - k) mod n)] where k is Element of NAT : k < n } holds
ex y, z being object st x = [y,z]
for x, y1, y2 being object st [x,y1] in { [k,((n - k) mod n)] where k is Element of NAT : k < n } & [x,y2] in { [k,((n - k) mod n)] where k is Element of NAT : k < n } holds
y1 = y2
proof
let x,
y1,
y2 be
object ;
( [x,y1] in { [k,((n - k) mod n)] where k is Element of NAT : k < n } & [x,y2] in { [k,((n - k) mod n)] where k is Element of NAT : k < n } implies y1 = y2 )
assume that A3:
[x,y1] in { [k,((n - k) mod n)] where k is Element of NAT : k < n }
and A4:
[x,y2] in { [k,((n - k) mod n)] where k is Element of NAT : k < n }
;
y1 = y2
consider k being
Element of
NAT such that A5:
[x,y1] = [k,((n - k) mod n)]
and
k < n
by A3;
A6:
y1 = (n - k) mod n
by A5, XTUPLE_0:1;
consider k9 being
Element of
NAT such that A7:
[x,y2] = [k9,((n - k9) mod n)]
and
k9 < n
by A4;
A8:
y2 = (n - k9) mod n
by A7, XTUPLE_0:1;
k =
x
by A5, XTUPLE_0:1
.=
k9
by A7, XTUPLE_0:1
;
hence
y1 = y2
by A6, A8;
verum
end;
then reconsider f = { [k,((n - k) mod n)] where k is Element of NAT : k < n } as Function by A2, FUNCT_1:def 1, RELAT_1:def 1;
A9:
for x being object st x in Segm n holds
x in dom f
for x being object st x in dom f holds
x in Segm n
then A14:
dom f = Segm n
by A9, TARSKI:2;
for y being object st y in rng f holds
y in Segm n
then
rng f c= Segm n
by TARSKI:def 3;
then reconsider f = f as UnOp of (Segm n) by A14, FUNCT_2:def 1, RELSET_1:4;
for k being Element of Segm n holds f . k = (n - k) mod n
hence
ex b1 being UnOp of (Segm n) st
for k being Element of Segm n holds b1 . k = (n - k) mod n
; verum