let n be positive Nat; :: thesis: Char (Z/ n) = n
set R = Z/ n;

per cases ( n = 1 or n > 1 ) by NAT_1:25;

suppose A1: n = 1 ; :: thesis: Char (Z/ n) = n

then A2: 1 '*' (1. (Z/ n)) = 0. (Z/ n) by Th59, INT_3:10;
for n being positive Nat st n < 1 holds
n '*' (1. (Z/ n)) <> 0. (Z/ n) by NAT_1:14;
hence Char (Z/ n) = n by A2, A1, Def5; :: thesis: verum

end;

suppose A3: n > 1 ; :: thesis: Char (Z/ n) = n

reconsider m = n - 1 as Nat ;
n - 1 < n - 0 by XREAL_1:15;
then reconsider mm = m as Element of Segm n by NAT_1:44;
reconsider e = 1 as Element of Segm n by A3, NAT_1:44;
A4: 1 '*' (1. (Z/ n)) = 1. (Z/ n) by Th59
.= 1 by INT_3:14, A3 ;
A5: for k being Nat st k <= m holds
k '*' (1. (Z/ n)) = k

proof

let k be Nat; :: thesis: ( k <= m implies k '*' (1. (Z/ n)) = k )
assume A6: k <= m ; :: thesis: k '*' (1. (Z/ n)) = k
defpred S₁[ Nat] means $1 '*' (1. (Z/ n)) = $1;
reconsider u = m as Element of NAT by INT_1:3;
0 '*' (1. (Z/ n)) = 0. (Z/ n) by Th58
.= 0 by NAT_1:44, SUBSET_1:def 8 ;
then A7: S₁[ 0 ] ;
A8: for k being Element of NAT st 0 <= k & k < u & S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( 0 <= k & k < u & S₁[k] implies S₁[k + 1] )
assume A9: ( 0 <= k & k < u ) ; :: thesis: ( not S₁[k] or S₁[k + 1] )
assume A10: S₁[k] ; :: thesis: S₁[k + 1]
reconsider z = k '*' (1. (Z/ n)) as Element of Segm n ;
A11: k + 1 < m + 1 by A9, XREAL_1:6;
(k + 1) '*' (1. (Z/ n)) = (k '*' (1. (Z/ n))) + (1. (Z/ n)) by Lm5
.= (k '*' (1. (Z/ n))) + (1 '*' (1. (Z/ n))) by Th59
.= k + 1 by INT_3:7, A11, A10, A4 ;
hence S₁[k + 1] ; :: thesis: verum

end;

A12: for i being Element of NAT st 0 <= i & i <= u holds
S₁[i] from INT_1:sch 7(A7, A8);
k is Element of NAT by INT_1:3;
hence k '*' (1. (Z/ n)) = k by A12, A6; :: thesis: verum

end;

A13: n '*' (1. (Z/ n)) = (m + 1) '*' (1. (Z/ n))
.= (m '*' (1. (Z/ n))) + (1. (Z/ n)) by Lm5
.= (m '*' (1. (Z/ n))) + (1 '*' (1. (Z/ n))) by Th59
.= (addint n) . (mm,e) by A4, A5
.= (m + 1) mod n by GR_CY_1:def 4
.= 0 by INT_1:50
.= 0. (Z/ n) by NAT_1:44, SUBSET_1:def 8 ;

now :: thesis: for k being positive Nat st k < n holds
k '*' (1. (Z/ n)) <> 0. (Z/ n)

let k be positive Nat; :: thesis: ( k < n implies k '*' (1. (Z/ n)) <> 0. (Z/ n) )
assume k < n ; :: thesis: k '*' (1. (Z/ n)) <> 0. (Z/ n)
then k < m + 1 ;
then A14: k <= m by NAT_1:13;

now :: thesis: not k '*' (1. (Z/ n)) = 0. (Z/ n)

assume k '*' (1. (Z/ n)) = 0. (Z/ n) ; :: thesis: contradiction
then k = 0. (Z/ n) by A5, A14
.= 0 by NAT_1:44, SUBSET_1:def 8 ;
hence contradiction ; :: thesis: verum

end;

hence k '*' (1. (Z/ n)) <> 0. (Z/ n) ; :: thesis: verum

end;

hence Char (Z/ n) = n by A13, Def5; :: thesis: verum

end;

end;