let p be Prime; :: thesis: for fp being FinSequence of NAT st p > 2 & ( for d being Nat st d in dom fp holds
(fp . d) gcd p = 1 ) holds
ex fr being FinSequence of INT st
( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = Lege (fp . d),p ) & Lege (Product fp),p = Product fr )
let fp be FinSequence of NAT ; :: thesis: ( p > 2 & ( for d being Nat st d in dom fp holds
(fp . d) gcd p = 1 ) implies ex fr being FinSequence of INT st
( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = Lege (fp . d),p ) & Lege (Product fp),p = Product fr ) )
assume A1: p > 2 ; :: thesis: ( ex d being Nat st
( d in dom fp & not (fp . d) gcd p = 1 ) or ex fr being FinSequence of INT st
( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = Lege (fp . d),p ) & Lege (Product fp),p = Product fr ) )
assume A2: for d being Nat st d in dom fp holds
(fp . d) gcd p = 1 ; :: thesis: ex fr being FinSequence of INT st
( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = Lege (fp . d),p ) & Lege (Product fp),p = Product fr )
(Product fp) gcd p = 1 by A2, WSIERP_1:43;
then A4: Lege (Product fp),p,(Product fp) |^ ((p -' 1) div 2) are_congruent_mod p by A1, Th28;
set k = (p -' 1) div 2;
set f = fp |^ ((p -' 1) div 2);
reconsider f = fp |^ ((p -' 1) div 2) as FinSequence of INT by FINSEQ_2:27, NUMBERS:17;
deffunc H₁( Nat) -> Integer = Lege (fp . $1),p;
consider fr being FinSequence such that
A5: ( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = H₁(d) ) ) from FINSEQ_1:sch 2();
for d being Nat st d in dom fr holds
fr . d in INT

proof

let d be Nat; :: thesis: ( d in dom fr implies fr . d in INT )
assume d in dom fr ; :: thesis: fr . d in INT
then fr . d = Lege (fp . d),p by A5;
hence fr . d in INT by INT_1:def 2; :: thesis: verum

end;

then reconsider fr = fr as FinSequence of INT by FINSEQ_2:14;
A6: len f = len fp by NAT_3:def 1;
for d being Nat st d in dom fr holds
fr . d,f . d are_congruent_mod p

proof

let d be Nat; :: thesis: ( d in dom fr implies fr . d,f . d are_congruent_mod p )
assume A7: d in dom fr ; :: thesis: fr . d,f . d are_congruent_mod p
then d in dom fp by A5, FINSEQ_3:31;
then (fp . d) gcd p = 1 by A2;
then Lege (fp . d),p,(fp . d) |^ ((p -' 1) div 2) are_congruent_mod p by A1, Th28;
then A8: fr . d,(fp . d) |^ ((p -' 1) div 2) are_congruent_mod p by A5, A7;
d in dom f by A5, A6, A7, FINSEQ_3:31;
hence fr . d,f . d are_congruent_mod p by A8, NAT_3:def 1; :: thesis: verum

end;

then Product fr, Product f are_congruent_mod p by A5, A6, Th32;
then A9: Product f, Product fr are_congruent_mod p by INT_1:35;
fp is FinSequence of REAL by FINSEQ_2:27;
then Lege (Product fp),p, Product f are_congruent_mod p by A4, NAT_3:15;
then Lege (Product fp),p, Product fr are_congruent_mod p by A9, INT_1:36;
then A10: p divides (Lege (Product fp),p) - (Product fr) by INT_2:19;
take fr ; :: thesis: ( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = Lege (fp . d),p ) & Lege (Product fp),p = Product fr )
A11: for d being Nat holds
( not d in dom fr or fr . d = 1 or fr . d = - 1 )

proof

let d be Nat; :: thesis: ( not d in dom fr or fr . d = 1 or fr . d = - 1 )
assume d in dom fr ; :: thesis: ( fr . d = 1 or fr . d = - 1 )
then fr . d = Lege (fp . d),p by A5;
hence ( fr . d = 1 or fr . d = - 1 ) by Th25; :: thesis: verum

end;

per cases ( Lege (Product fp),p = 1 or Lege (Product fp),p = - 1 ) by Th25;

suppose A12: Lege (Product fp),p = 1 ; :: thesis: ( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = Lege (fp . d),p ) & Lege (Product fp),p = Product fr )

then Product fr <> - 1 by A1, A10, NAT_D:7;
hence ( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = Lege (fp . d),p ) & Lege (Product fp),p = Product fr ) by A5, A11, A12, Th31; :: thesis: verum

end;

suppose A13: Lege (Product fp),p = - 1 ; :: thesis: ( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = Lege (fp . d),p ) & Lege (Product fp),p = Product fr )

now

assume Product fr = 1 ; :: thesis: contradiction
then p divides - 2 by A10, A13;
then p divides 2 by INT_2:14;
hence contradiction by A1, NAT_D:7; :: thesis: verum

end;

hence ( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = Lege (fp . d),p ) & Lege (Product fp),p = Product fr ) by A5, A11, A13, Th31; :: thesis: verum

end;

end;