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 ) )

deffunc H1( Nat) -> Integer = Lege ((fp . \$1),p);
set k = (p -' 1) div 2;
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 )

set f = fp |^ ((p -' 1) div 2);
reconsider f = fp |^ ((p -' 1) div 2) as FinSequence of INT by ;
consider fr being FinSequence such that
A3: ( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = H1(d) ) ) from 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 A3;
hence fr . d in INT by INT_1:def 2; :: thesis: verum
end;
then reconsider fr = fr as FinSequence of INT by FINSEQ_2:12;
A4: fp is FinSequence of REAL by ;
A5: 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 A6: d in dom fr ; :: thesis: fr . d,f . d are_congruent_mod p
then d in dom fp by ;
then (fp . d) gcd p = 1 by A2;
then Lege ((fp . d),p),(fp . d) |^ ((p -' 1) div 2) are_congruent_mod p by ;
then A7: fr . d,(fp . d) |^ ((p -' 1) div 2) are_congruent_mod p by A3, A6;
d in dom f by ;
hence fr . d,f . d are_congruent_mod p by ; :: thesis: verum
end;
then A8: Product f, Product fr are_congruent_mod p by ;
(Product fp) gcd p = 1 by ;
then Lege ((Product fp),p),(Product fp) |^ ((p -' 1) div 2) are_congruent_mod p by ;
then Lege ((Product fp),p), Product f are_congruent_mod p by ;
then Lege ((Product fp),p), Product fr are_congruent_mod p by ;
then A9: p divides (Lege ((Product fp),p)) - (Product fr) ;
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 )

A10: for d being Nat holds
( not d in dom fr or fr . d = 1 or fr . d = 0 or fr . d = - 1 )
proof
let d be Nat; :: thesis: ( not d in dom fr or fr . d = 1 or fr . d = 0 or fr . d = - 1 )
assume d in dom fr ; :: thesis: ( fr . d = 1 or fr . d = 0 or fr . d = - 1 )
then fr . d = Lege ((fp . d),p) by A3;
hence ( fr . d = 1 or fr . d = 0 or fr . d = - 1 ) by Th25; :: thesis: verum
end;
per cases ( Lege ((Product fp),p) = 1 or Lege ((Product fp),p) = 0 or Lege ((Product fp),p) = - 1 ) by Th25;
suppose A11: 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 A12: Product fr <> - 1 by ;
now :: thesis: not Product fr = 0
assume Product fr = 0 ; :: thesis: contradiction
then p = 1 by ;
hence contradiction by A1; :: 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 A3, A10, A11, Th31, A12; :: thesis: verum
end;
suppose A13: Lege ((Product fp),p) = 0 ; :: 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 )

A14: now :: thesis: not Product fr = - 1
assume Product fr = - 1 ; :: thesis: contradiction
then p = 1 by ;
hence contradiction by A1; :: 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 A3, A10, A13, Th31, A14; :: thesis: verum
end;
suppose A15: 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 )

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 A3, A10, A15, Th31, A16; :: thesis: verum
end;
end;