let p be Prime; :: thesis:
let fp be FinSequence of NAT ; :: thesis:
assume A1: p > 2 ; :: thesis:
deffunc H₁( 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:
set f = fp |^ ((p -' 1) div 2);
reconsider f = fp |^ ((p -' 1) div 2) as FinSequence of INT by FINSEQ_2:24, NUMBERS:17;
consider fr being FinSequence such that
A3: ( 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:
assume d in dom fr ; :: thesis:
then fr . d = Lege ((fp . d),p) by A3;
hence fr . d in INT by INT_1:def 2; :: thesis:

end;

then reconsider fr = fr as FinSequence of INT by FINSEQ_2:12;
A4: fp is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;
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:
assume A6: d in dom fr ; :: thesis:
then d in dom fp by A3, FINSEQ_3:29;
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 A7: fr . d,(fp . d) |^ ((p -' 1) div 2) are_congruent_mod p by A3, A6;
d in dom f by A3, A5, A6, FINSEQ_3:29;
hence fr . d,f . d are_congruent_mod p by A7, NAT_3:def 1; :: thesis:

end;

then A8: Product f, Product fr are_congruent_mod p by A3, A5, Th32, INT_1:14;
(Product fp) gcd p = 1 by A2, WSIERP_1:36;
then Lege ((Product fp),p),(Product fp) |^ ((p -' 1) div 2) are_congruent_mod p by A1, Th28;
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 A8, INT_1:15;
then A9: p divides (Lege ((Product fp),p)) - (Product fr) ;
take fr ; :: thesis:
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:
assume d in dom fr ; :: thesis:
then fr . d = Lege ((fp . d),p) by A3;
hence ( fr . d = 1 or fr . d = 0 or fr . d = - 1 ) by Th25; :: thesis:

end;

per cases by Th25;

suppose A11: Lege ((Product fp),p) = 1 ; :: thesis:

then A12: Product fr <> - 1 by A1, A9, NAT_D:7;

now :: thesis:

assume Product fr = 0 ; :: thesis:
then p = 1 by A9, A11, WSIERP_1:15;
hence contradiction by A1; :: thesis:

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:

end;

suppose A13: Lege ((Product fp),p) = 0 ; :: thesis:

A14: now :: thesis:

assume Product fr = - 1 ; :: thesis:
then p = 1 by A9, A13, WSIERP_1:15;
hence contradiction by A1; :: thesis:

end;

now :: thesis:

assume Product fr = 1 ; :: thesis:
then p divides 1 by A9, A13, INT_2:10;
then p = 1 by WSIERP_1:15;
hence contradiction by A1; :: thesis:

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:

end;

suppose A15: Lege ((Product fp),p) = - 1 ; :: thesis:

A16: now :: thesis:

assume Product fr = 1 ; :: thesis:
then p divides - 2 by A9, A15;
then p divides 2 by INT_2:10;
hence contradiction by A1, NAT_D:7; :: thesis:

end;

now :: thesis:

assume Product fr = 0 ; :: thesis:
then p divides 1 by A9, A15, INT_2:10;
then p = 1 by WSIERP_1:15;
hence contradiction by A1; :: thesis:

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, A15, Th31, A16; :: thesis:

end;

end;