let p be FinSequence; :: thesis: ( len p is prime & ex i being Nat st
( 0 < i & i < len p & p = (p /^ i) ^ (p | i) ) implies rng p c= {(p . 1)} )
set L = len p;
assume A1: len p is prime ; :: thesis: ( for i being Nat holds
( not 0 < i or not i < len p or not p = (p /^ i) ^ (p | i) ) or rng p c= {(p . 1)} )
reconsider P = p as FinSequence of (rng p) \/ {1} by XBOOLE_1:7, FINSEQ_1:def 4;
given j being Nat such that A2: 0 < j and
A3: j < len p and
A4: p = (p /^ j) ^ (p | j) ; :: thesis: rng p c= {(p . 1)}
defpred S₁[ Nat] means p . 1 = p . (((j * $1) mod (len p)) + 1);
set p1j = p /^ j;
set pj = p | j;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
set k1 = k + 1;
set jk = (j * k) mod (len p);
j * (k + 1) = (j * k) + j ;
then A7: (j * (k + 1)) mod (len p) = (((j * k) mod (len p)) + j) mod (len p) by NAT_D:23;
A8: len (p | j) = j by A3, FINSEQ_1:59;
A9: len (p /^ j) = (len p) - j by A3, RFINSEQ:def 1;
((j * k) mod (len p)) + 1 <= len p by NAT_D:1, A3, NAT_1:13;
then A10: ((j * k) mod (len p)) + 1 in dom p by NAT_1:11, FINSEQ_3:25;

per cases ( ((j * k) mod (len p)) + 1 in dom (p /^ j) or ex n being Nat st
( n in dom (p | j) & ((j * k) mod (len p)) + 1 = (len (p /^ j)) + n ) ) by A4, A10, FINSEQ_1:25;

suppose A11: ((j * k) mod (len p)) + 1 in dom (p /^ j) ; :: thesis: S₁[k + 1]

then ((j * k) mod (len p)) + 1 <= (len p) - j by A9, FINSEQ_3:25;
then (((j * k) mod (len p)) + 1) + j <= ((len p) - j) + j by XREAL_1:6;
then (((j * k) mod (len p)) + j) + 1 <= len p ;
then ((j * k) mod (len p)) + j < len p by NAT_1:13;
then A12: (((j * k) mod (len p)) + j) mod (len p) = ((j * k) mod (len p)) + j by NAT_D:24;
p . (((j * k) mod (len p)) + 1) = (p /^ j) . (((j * k) mod (len p)) + 1) by A11, A4, FINSEQ_1:def 7
.= p . ((((j * k) mod (len p)) + 1) + j) by A3, A11, RFINSEQ:def 1 ;
hence S₁[k + 1] by A12, A7, A6; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom (p | j) & ((j * k) mod (len p)) + 1 = (len (p /^ j)) + n ) ; :: thesis: S₁[k + 1]

then consider n being Nat such that
A13: n in dom (p | j) and
A14: ((j * k) mod (len p)) + 1 = (len (p /^ j)) + n ;
len (p | j) >= n by A13, FINSEQ_3:25;
then A15: n < len p by A8, A3, XXREAL_0:2;
reconsider n1 = n - 1 as Nat by A13, FINSEQ_3:25, NAT_1:21;
n1 < n1 + 1 by NAT_1:13;
then A16: n1 < len p by A15, XXREAL_0:2;
((j * k) mod (len p)) + j = (1 * (len p)) + n1 by A14, A9;
then A17: (((j * k) mod (len p)) + j) mod (len p) = n1 mod (len p) by NAT_D:21
.= n1 by A16, NAT_D:24 ;
p . (((j * k) mod (len p)) + 1) = (p | j) . n by A4, A13, A14, FINSEQ_1:def 7
.= p . n by A13, FUNCT_1:47 ;
hence S₁[k + 1] by A17, A7, A6; :: thesis: verum

end;

end;

end;

(j * 0) mod (len p) = 0 by NAT_D:26;
then A18: S₁[ 0 ] ;
A19: for k being Nat holds S₁[k] from NAT_1:sch 2(A18, A5);
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in {(p . 1)} )
assume y in rng p ; :: thesis: y in {(p . 1)}
then consider m being object such that
A20: m in dom p and
A21: p . m = y by FUNCT_1:def 3;
reconsider m = m as Nat by A20;
A22: m <= len p by A20, FINSEQ_3:25;
reconsider m1 = m - 1 as Nat by A20, FINSEQ_3:25, NAT_1:21;

per cases ( m = 1 or m <> 1 ) ;

suppose m = 1 ; :: thesis: y in {(p . 1)}

hence y in {(p . 1)} by A21, TARSKI:def 1; :: thesis: verum

end;

suppose m <> 1 ; :: thesis: y in {(p . 1)}

j gcd (len p) = 1

proof

j gcd (len p) divides len p by INT_2:def 2;
then A23: ( j gcd (len p) = 1 or j gcd (len p) = len p ) by A1, INT_2:def 4;
assume j gcd (len p) <> 1 ; :: thesis: contradiction
then len p divides j by A23, INT_2:def 2;
hence contradiction by A2, NAT_D:7, A3; :: thesis: verum

end;

then consider n being Nat such that
A24: ((j * n) - m1) mod (len p) = 0 by INT_2:def 3, A3, INT_4:16;
A25: m1 + 1 = m ;
then m1 < len p by A22, NAT_1:13;
then m1 mod (len p) = m1 by NAT_D:24;
then (j * n) mod (len p) = m1 by A3, INT_4:22, A24;
then p . 1 = p . m by A25, A19;
hence y in {(p . 1)} by TARSKI:def 1, A21; :: thesis: verum

end;

end;