let a, m be Nat; :: thesis:
assume that
A1: a <> 0 and
A2: m > 1 and
A3: a,m are_relative_prime ; :: thesis:
set X = { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ;
A4: a |^ (Euler m) <> 0 by A1, PREPOWER:5;
set Y = { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } ;
A5: for x being Nat st x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } holds
(a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) }

proof

let x be Nat; :: thesis:
assume x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; :: thesis:
then consider t being Element of NAT such that
A6: t = x and
A7: m,t are_relative_prime and
A8: t >= 1 and
t <= m ;
A9: a * t,m are_relative_prime by A1, A2, A3, A7, EULER_1:14;
(a * t) mod m <> 0

proof

assume (a * t) mod m = 0 ; :: thesis:
then consider s being Nat such that
A10: a * t = (m * s) + 0 and
0 < m by A2, NAT_D:def 2;
s gcd 1 = 1 by NEWTON:51;
then (m * s) gcd (m * 1) = m by EULER_1:5;
hence contradiction by A2, A9, A10, INT_2:def 3; :: thesis:

end;

then A11: (a * t) mod m >= 1 by NAT_1:14;
A12: (a * t) mod m <= m by A2, NAT_D:1;
m,(a * t) mod m are_relative_prime by A1, A2, A3, A7, A8, Th5;
hence (a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A6, A11, A12; :: thesis:

end;

A13: { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } = { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) }

proof

thus { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } c= { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; :: thesis:
then consider xx being Element of NAT such that
A14: x = xx and
A15: m,xx are_relative_prime and
xx >= 1 and
A16: xx <= m ;
consider i, j being Integer such that
A17: (i * a) + (j * m) = xx by A3, EULER_1:10;
xx <> m by A2, A15, EULER_1:1;
then xx < m by A16, XXREAL_0:1;
then A18: xx mod m = xx by NAT_D:24;
reconsider im = i mod m as Element of NAT by INT_1:3, NEWTON:64;
i mod m <> 0

proof

assume i mod m = 0 ; :: thesis:
then 0 = i - ((i div m) * m) by A2, INT_1:def 10;
then m gcd xx = (m * 1) gcd (m * (((i div m) * a) + j)) by A17
.= m * (1 gcd (((i div m) * a) + j)) by A2, EULER_1:15
.= m * 1 by Lm3
.= m ;
hence contradiction by A2, A15, INT_2:def 3; :: thesis:

end;

then A19: im >= 1 by NAT_1:14;
A20: i = ((i div m) * m) + (i mod m) by A2, NEWTON:66;
then reconsider ij = ((i mod m) * a) + ((((i div m) * a) + j) * m) as Element of NAT by A17;
A21: im <= m by A2, NEWTON:65;
A22: ij mod m = (im * a) mod m by EULER_1:12;
then m,im are_relative_prime by A2, A15, A18, A17, A20, Th6;
then im in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A19, A21;
hence x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } by A14, A18, A17, A20, A22; :: thesis:

end;

A23: for xi, xj being Nat st xi in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xj in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xi <> xj holds
(a * xi) mod m <> (a * xj) mod m

proof

let xi, xj be Nat; :: thesis:
assume that
A24: xi in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } and
A25: xj in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } and
A26: xi <> xj ; :: thesis:
set tm = (a * xi) mod m;
set sm = (a * xj) mod m;
assume A27: (a * xi) mod m = (a * xj) mod m ; :: thesis:
consider s being Element of NAT such that
A28: s = xj and
m,s are_relative_prime and
A29: ( s >= 1 & s <= m ) by A25;
A30: (a * xj) mod m = (a * s) - (m * ((a * s) div m)) by A2, A28, NEWTON:63;
consider t being Element of NAT such that
A31: t = xi and
m,t are_relative_prime and
A32: ( t >= 1 & t <= m ) by A24;
(a * xi) mod m = (a * t) - (m * ((a * t) div m)) by A2, A31, NEWTON:63;
then 0 = (a * (t - s)) - (m * (((a * t) div m) - ((a * s) div m))) by A27, A30;
then A33: m divides a * (t - s) by INT_1:def 3;
reconsider m = m, c = t - s as Integer ;
( 1 - m <= c & c <= m - 1 ) by A32, A29, XREAL_1:13;
then t - s = 0 by A3, A33, Lm4, INT_2:25;
hence contradiction by A26, A31, A28; :: thesis:

end;

reconsider FX = Sgm { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } as FinSequence of NAT ;
reconsider FYY = a * FX as FinSequence of NAT ;
reconsider FY = FYY mod m as FinSequence of NAT ;
A34: { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } c= Seg m

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; :: thesis:
then ex xx being Element of NAT st
( x = xx & m,xx are_relative_prime & xx >= 1 & xx <= m ) ;
hence x in Seg m by FINSEQ_1:1; :: thesis:

end;

then reconsider X = { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } as finite set ;
dom FYY = Seg (len FYY) by FINSEQ_1:def 3
.= Seg (len FX) by NEWTON:2 ;
then A35: dom FX = dom FYY by FINSEQ_1:def 3;
A36: dom FY = Seg (len FY) by FINSEQ_1:def 3
.= Seg (len FYY) by Def1
.= Seg (len FX) by NEWTON:2 ;
then A37: dom FX = dom FY by FINSEQ_1:def 3;
A38: rng FY = { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) }

proof

thus rng FY c= { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng FY ; :: thesis:
then consider y being set such that
A39: y in dom FY and
A40: x = FY . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A39;
FX . y in rng FX by A37, A39, FUNCT_1:def 3;
then A41: FX . y in X by A34, FINSEQ_1:def 13;
y in dom FX by A36, A39, FINSEQ_1:def 3;
then FY . y = (FYY . y) mod m by A35, Def1
.= (a * (FX . y)) mod m by RVSUM_1:44 ;
hence x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } by A40, A41; :: thesis:

end;

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } ; :: thesis:
then consider yy being Element of NAT such that
A42: y = yy and
A43: ex u being Element of NAT st
( yy = (a * u) mod m & u in X ) ;
consider uu being Element of NAT such that
A44: yy = (a * uu) mod m and
A45: uu in X by A43;
uu in rng FX by A34, A45, FINSEQ_1:def 13;
then consider xx being set such that
A46: xx in dom FX and
A47: uu = FX . xx by FUNCT_1:def 3;
reconsider xx = xx as Element of NAT by A46;
FY . xx = (FYY . xx) mod m by A35, A46, Def1
.= y by A42, A44, A47, RVSUM_1:44 ;
hence y in rng FY by A37, A46, FUNCT_1:def 3; :: thesis:

end;

A48: FY is one-to-one

proof

A49: FX is one-to-one by A34, FINSEQ_3:92;
let x1, x2 be set ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A50: x1 in dom FY and
A51: x2 in dom FY and
A52: FY . x1 = FY . x2 ; :: thesis:
A53: x2 in dom FX by A36, A51, FINSEQ_1:def 3;
reconsider x2 = x2 as Element of NAT by A51;
A54: x1 in dom FX by A36, A50, FINSEQ_1:def 3;
reconsider x1 = x1 as Element of NAT by A50;
A55: ( FX . x1 in rng FX & FX . x2 in rng FX ) by A37, A50, A51, FUNCT_1:def 3;
A56: FY . x2 = (FYY . x2) mod m by A35, A53, Def1
.= (a * (FX . x2)) mod m by RVSUM_1:44 ;
FY . x1 = (FYY . x1) mod m by A35, A54, Def1
.= (a * (FX . x1)) mod m by RVSUM_1:44 ;
then ( not FX . x1 in X or not FX . x2 in X or not FX . x1 <> FX . x2 ) by A23, A52, A56;
hence x1 = x2 by A34, A54, A53, A55, A49, FINSEQ_1:def 13, FUNCT_1:def 4; :: thesis:

end;

for x being set holds card (Coim (FX,x)) = card (Coim (FY,x))

proof

let x be set ; :: thesis:

now

per cases ;

suppose A57: x in X ; :: thesis:

A58: FX is one-to-one by A34, FINSEQ_3:92;
x in rng FX by A34, A57, FINSEQ_1:def 13;
then A59: len (FX - {x}) = (len FX) - 1 by A58, FINSEQ_3:90;
A60: ( (len (FX - {x})) - (len (FX - {x})) = ((len FX) - (card (FX " {x}))) - (len (FX - {x})) & len (FY - {x}) = (len FY) - (card (FY " {x})) ) by FINSEQ_3:59;
len (FY - {x}) = (len FY) - 1 by A13, A38, A48, A57, FINSEQ_3:90;
hence card (Coim (FX,x)) = card (Coim (FY,x)) by A59, A60; :: thesis:

end;

suppose not x in X ; :: thesis:

then ( not x in rng FX & FY " {x} = {} ) by A13, A34, A38, FINSEQ_1:def 13, FUNCT_1:72;
hence card (Coim (FX,x)) = card (Coim (FY,x)) by FUNCT_1:72; :: thesis:

end;

hence card (Coim (FX,x)) = card (Coim (FY,x)) ; :: thesis:

end;

then A61: FX,FY are_fiberwise_equipotent by CLASSES1:def 9;
then A62: len FX = len FY by RFINSEQ:3;
A63: (Product FY) mod m = ((a |^ (len FY)) * (Product FX)) mod m

proof

proof

let n be Nat; :: thesis:

now

per cases ;

suppose A66: n + 1 <= len FY ; :: thesis:

end;

suppose n + 1 > len FY ; :: thesis:

hence ( S₁[n] implies S₁[n + 1] ) ; :: thesis:

end;

hence ( S₁[n] implies S₁[n + 1] ) ; :: thesis:

end;

FX | (len FX) = FX | (Seg (len FX)) by FINSEQ_1:def 15;
then A77: FX = FX | (len FY) by A62, FINSEQ_2:20;
A78: S₁[ 0 ] by NEWTON:4, RVSUM_1:94;
for n being Nat holds S₁[n] from NAT_1:sch 2(A78, A65);
hence (Product FY) mod m = ((a |^ (len FY)) * (Product FX)) mod m by A64, A77; :: thesis:

end;

A79: Product FX,m are_relative_prime

proof

defpred S₁[ Nat] means ( $1 <= len FX implies Product (FX | $1),m are_relative_prime );
A80: FX | (len FX) = FX by FINSEQ_1:58;
A81: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:

now

per cases ;

suppose A82: len FX >= n + 1 ; :: thesis:

reconsider FF = FX | (n + 1) as FinSequence of NAT ;
reconsider ff = FF . (n + 1) as Element of NAT ;
len FF = n + 1 by A82, FINSEQ_1:59;
then A83: FF = (FF | n) ^ <*ff*> by RFINSEQ:7;
reconsider a = Product (FF | n), b = ff, m9 = m as Integer ;
A84: n <= n + 1 by NAT_1:11;
0 + 1 <= n + 1 by XREAL_1:6;
then ( (FX | (n + 1)) . (n + 1) = FX . (n + 1) & n + 1 in dom FX ) by A82, FINSEQ_3:25, FINSEQ_3:112;
then A85: (FX | (n + 1)) . (n + 1) in rng FX by FUNCT_1:def 3;
rng FX = X by A34, FINSEQ_1:def 13;
then A86: ex p being Element of NAT st
( ff = p & m,p are_relative_prime & p >= 1 & p <= m ) by A85;
assume S₁[n] ; :: thesis:
then a,m9 are_relative_prime by A82, A84, FINSEQ_5:77, XXREAL_0:2;
then a * b,m9 are_relative_prime by A86, INT_2:26;
hence S₁[n + 1] by A83, RVSUM_1:96; :: thesis:

end;

suppose len FX < n + 1 ; :: thesis:

hence ( S₁[n] implies S₁[n + 1] ) ; :: thesis:

end;

hence ( S₁[n] implies S₁[n + 1] ) ; :: thesis:

end;

(Product (FX | 0)) gcd m = 1 by NEWTON:51, RVSUM_1:94;
then A87: S₁[ 0 ] by INT_2:def 3;
for n being Nat holds S₁[n] from NAT_1:sch 2(A87, A81);
hence Product FX,m are_relative_prime by A80; :: thesis:

end;

len FX = card X by A34, FINSEQ_3:39
.= Euler m by EULER_1:def 1 ;
then A88: len FY = Euler m by A61, RFINSEQ:3;
(Product FX) mod m = (Product FY) mod m by A61, Th25;
hence (a |^ (Euler m)) mod m = 1 by A2, A63, A88, A4, A79, Th27; :: thesis: