reconsider n = n as non zero natural number by A1;
set f = { [k,((n - k) mod n)] where k is Element of NAT : k < n } ;
A2: { [k,((n - k) mod n)] where k is Element of NAT : k < n } is Relation-like

proof

for x being set st x in { [k,((n - k) mod n)] where k is Element of NAT : k < n } holds
ex y, z being set st x = [y,z]

proof

let x be set ; :: thesis: ( x in { [k,((n - k) mod n)] where k is Element of NAT : k < n } implies ex y, z being set 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 set st x = [y,z]
then consider k being Element of NAT such that
A3: ( x = [k,((n - k) mod n)] & k < n ) ;
thus ex y, z being set st x = [y,z] by A3; :: thesis: verum

end;

hence { [k,((n - k) mod n)] where k is Element of NAT : k < n } is Relation-like by RELAT_1:def 1; :: thesis: verum

end;

{ [k,((n - k) mod n)] where k is Element of NAT : k < n } is Function-like

proof

for x, y1, y2 being set 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 set ; :: 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 A4: ( [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 } ) ; :: thesis: y1 = y2
then consider k being Element of NAT such that
A5: ( [x,y1] = [k,((n - k) mod n)] & k < n ) ;
consider k' being Element of NAT such that
A6: ( [x,y2] = [k',((n - k') mod n)] & k' < n ) by A4;
A7: k = [x,y1] `1 by A5, MCART_1:def 1
.= x by MCART_1:def 1
.= [k',((n - k') mod n)] `1 by A6, MCART_1:def 1
.= k' by MCART_1:def 1 ;
A8: y1 = [k,((n - k) mod n)] `2 by A5, MCART_1:def 2
.= (n - k) mod n by MCART_1:def 2 ;
y2 = [k',((n - k') mod n)] `2 by A6, MCART_1:def 2
.= (n - k') mod n by MCART_1:def 2 ;
hence y1 = y2 by A7, A8; :: thesis: verum

end;

hence { [k,((n - k) mod n)] where k is Element of NAT : k < n } is Function-like by FUNCT_1:def 1; :: thesis: verum

end;

then reconsider f = { [k,((n - k) mod n)] where k is Element of NAT : k < n } as Function by A2;
A9: dom f = Segm n

proof

A10: for x being set st x in dom f holds
x in Segm n

proof

let x be set ; :: thesis: ( x in dom f implies x in Segm n )
assume x in dom f ; :: thesis: x in Segm n
then consider y being set such that
A11: [x,y] in f by RELAT_1:def 4;
consider k being Element of NAT such that
A12: ( [x,y] = [k,((n - k) mod n)] & k < n ) by A11;
x = [k,((n - k) mod n)] `1 by A12, MCART_1:def 1
.= k by MCART_1:def 1 ;
hence x in Segm n by A12, GR_CY_1:10; :: thesis: verum

end;

for x being set st x in Segm n holds
x in dom f

proof

let x be set ; :: thesis: ( x in Segm n implies x in dom f )
assume A13: x in Segm n ; :: thesis: x in dom f
then reconsider x = x as Element of NAT ;
x < n by A13, GR_CY_1:10;
then [x,((n - x) mod n)] in f ;
hence x in dom f by RELAT_1:def 4; :: thesis: verum

end;

hence dom f = Segm n by A10, TARSKI:2; :: thesis: verum

end;

rng f c= Segm n

proof

for y being set st y in rng f holds
y in Segm n

proof

let y be set ; :: thesis: ( y in rng f implies y in Segm n )
assume y in rng f ; :: thesis: y in Segm n
then consider x being set such that
A14: [x,y] in f by RELAT_1:def 5;
consider k being Element of NAT such that
A15: ( [x,y] = [k,((n - k) mod n)] & k < n ) by A14;
A16: y = [k,((n - k) mod n)] `2 by A15, MCART_1:def 2
.= (n - k) mod n by MCART_1:def 2 ;
k - k < n - k by A15, XREAL_1:11;
then reconsider z = n - k as Element of NAT by INT_1:16;
z mod n < n by NAT_D:1;
hence y in Segm n by A16, GR_CY_1:10; :: thesis: verum

end;

hence rng f c= Segm n by TARSKI:def 3; :: thesis: verum

end;

then reconsider f = f as UnOp of (Segm n) by A9, FUNCT_2:def 1, RELSET_1:11;
for k being Element of Segm n holds f . k = (n - k) mod n

proof

let k be Element of Segm n; :: thesis: f . k = (n - k) mod n
reconsider k = k as Element of NAT ;
k < n by GR_CY_1:10;
then [k,((n - k) mod n)] in f ;
hence f . k = (n - k) mod n by A9, FUNCT_1:def 4; :: thesis: verum

end;

hence ex b₁ being UnOp of (Segm n) st
for k being Element of Segm n holds b₁ . k = (n - k) mod n ; :: thesis: verum