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]

y1 = y2

A9: for x being object st x in Segm n holds

x in dom f

x in Segm n

for y being object st y in rng f holds

y in Segm n

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_{1} being UnOp of (Segm n) st

for k being Element of Segm n holds b_{1} . k = (n - k) mod n
; :: thesis: verum

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]

proof

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
let x be object ; :: thesis: ( x in { [k,((n - k) mod n)] where k is Element of NAT : k < n } implies ex y, z being object st x = [y,z] )

assume x in { [k,((n - k) mod n)] where k is Element of NAT : k < n } ; :: thesis: ex y, z being object st x = [y,z]

then ex k being Element of NAT st

( x = [k,((n - k) mod n)] & k < n ) ;

hence ex y, z being object st x = [y,z] ; :: thesis: verum

end;assume x in { [k,((n - k) mod n)] where k is Element of NAT : k < n } ; :: thesis: ex y, z being object st x = [y,z]

then ex k being Element of NAT st

( x = [k,((n - k) mod n)] & k < n ) ;

hence ex y, z being object st x = [y,z] ; :: thesis: verum

y1 = y2

proof

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;
let x, y1, y2 be object ; :: thesis: ( [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 } ; :: thesis: 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; :: thesis: verum

end;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 } ; :: thesis: 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; :: thesis: verum

A9: for x being object st x in Segm n holds

x in dom f

proof

for x being object st x in dom f holds
let x be object ; :: thesis: ( x in Segm n implies x in dom f )

assume A10: x in Segm n ; :: thesis: x in dom f

then reconsider x = x as Element of NAT ;

x < n by A10, NAT_1:44;

then [x,((n - x) mod n)] in f ;

hence x in dom f by XTUPLE_0:def 12; :: thesis: verum

end;assume A10: x in Segm n ; :: thesis: x in dom f

then reconsider x = x as Element of NAT ;

x < n by A10, NAT_1:44;

then [x,((n - x) mod n)] in f ;

hence x in dom f by XTUPLE_0:def 12; :: thesis: verum

x in Segm n

proof

then A14:
dom f = Segm n
by A9, TARSKI:2;
let x be object ; :: thesis: ( x in dom f implies x in Segm n )

assume x in dom f ; :: thesis: x in Segm n

then consider y being object such that

A11: [x,y] in f by XTUPLE_0:def 12;

consider k being Element of NAT such that

A12: [x,y] = [k,((n - k) mod n)] and

A13: k < n by A11;

x = k by A12, XTUPLE_0:1;

hence x in Segm n by A13, NAT_1:44; :: thesis: verum

end;assume x in dom f ; :: thesis: x in Segm n

then consider y being object such that

A11: [x,y] in f by XTUPLE_0:def 12;

consider k being Element of NAT such that

A12: [x,y] = [k,((n - k) mod n)] and

A13: k < n by A11;

x = k by A12, XTUPLE_0:1;

hence x in Segm n by A13, NAT_1:44; :: thesis: verum

for y being object st y in rng f holds

y in Segm n

proof

then
rng f c= Segm n
by TARSKI:def 3;
let y be object ; :: thesis: ( y in rng f implies y in Segm n )

assume y in rng f ; :: thesis: y in Segm n

then consider x being object such that

A15: [x,y] in f by XTUPLE_0:def 13;

consider k being Element of NAT such that

A16: [x,y] = [k,((n - k) mod n)] and

A17: k < n by A15;

k - k < n - k by A17, XREAL_1:9;

then reconsider z = n - k as Element of NAT by INT_1:3;

A18: z mod n < n by NAT_D:1;

y = (n - k) mod n by A16, XTUPLE_0:1;

hence y in Segm n by A18, NAT_1:44; :: thesis: verum

end;assume y in rng f ; :: thesis: y in Segm n

then consider x being object such that

A15: [x,y] in f by XTUPLE_0:def 13;

consider k being Element of NAT such that

A16: [x,y] = [k,((n - k) mod n)] and

A17: k < n by A15;

k - k < n - k by A17, XREAL_1:9;

then reconsider z = n - k as Element of NAT by INT_1:3;

A18: z mod n < n by NAT_D:1;

y = (n - k) mod n by A16, XTUPLE_0:1;

hence y in Segm n by A18, NAT_1:44; :: thesis: verum

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

proof

hence
ex b
let k be Element of Segm n; :: thesis: f . k = (n - k) mod n

reconsider k = k as Element of NAT ;

A0: (n - k) mod n is set by TARSKI:1;

k < n by NAT_1:44;

then [k,((n - k) mod n)] in f ;

hence f . k = (n - k) mod n by A14, A0, FUNCT_1:def 2; :: thesis: verum

end;reconsider k = k as Element of NAT ;

A0: (n - k) mod n is set by TARSKI:1;

k < n by NAT_1:44;

then [k,((n - k) mod n)] in f ;

hence f . k = (n - k) mod n by A14, A0, FUNCT_1:def 2; :: thesis: verum

for k being Element of Segm n holds b