let p be Prime; :: thesis: ( p > 2 implies ex fp being FinSequence of NAT st
( len fp = (p -' 1) div 2 & ( for d being Nat st d in dom fp holds
(fp . d) gcd p = 1 ) & ( for d being Nat st d in dom fp holds
fp . d is_quadratic_residue_mod p ) & ( for d, e being Nat st d in dom fp & e in dom fp & d <> e holds
not fp . d,fp . e are_congruent_mod p ) ) )

deffunc H1( Nat) -> Element of omega = \$1 ^2 ;
consider fp being FinSequence such that
A1: ( len fp = (p -' 1) div 2 & ( for d being Nat st d in dom fp holds
fp . d = H1(d) ) ) from for d being Nat st d in dom fp holds
fp . d in NAT
proof
let d be Nat; :: thesis: ( d in dom fp implies fp . d in NAT )
assume d in dom fp ; :: thesis: fp . d in NAT
then fp . d = d ^2 by A1;
hence fp . d in NAT ; :: thesis: verum
end;
then reconsider fp = fp as FinSequence of NAT by FINSEQ_2:12;
A2: p > 1 by INT_2:def 4;
then A3: p -' 1 = p - 1 by XREAL_1:233;
assume p > 2 ; :: thesis: ex fp being FinSequence of NAT st
( len fp = (p -' 1) div 2 & ( for d being Nat st d in dom fp holds
(fp . d) gcd p = 1 ) & ( for d being Nat st d in dom fp holds
fp . d is_quadratic_residue_mod p ) & ( for d, e being Nat st d in dom fp & e in dom fp & d <> e holds
not fp . d,fp . e are_congruent_mod p ) )

then p is odd by PEPIN:17;
then p - 1 is even by HILBERT3:2;
then 2 divides p -' 1 by ;
then (p -' 1) mod 2 = 0 by PEPIN:6;
then A4: (p -' 1) div 2 = (p -' 1) / 2 by PEPIN:63;
A5: for d, e being Nat st d in dom fp & e in dom fp & d <> e holds
not fp . d,fp . e are_congruent_mod p
proof
p - 1 > 0 by ;
then (p - 1) / 2 < (p - 1) / 1 by XREAL_1:76;
then (p -' 1) div 2 < p by ;
then A6: ((p -' 1) div 2) - 1 < p by XREAL_1:147;
let d, e be Nat; :: thesis: ( d in dom fp & e in dom fp & d <> e implies not fp . d,fp . e are_congruent_mod p )
assume that
A7: d in dom fp and
A8: e in dom fp and
A9: d <> e ; :: thesis: not fp . d,fp . e are_congruent_mod p
A10: e in Seg ((p -' 1) div 2) by ;
then A11: e <= (p -' 1) div 2 by FINSEQ_1:1;
A12: d in Seg ((p -' 1) div 2) by ;
then A13: d >= 1 by FINSEQ_1:1;
then 1 - ((p -' 1) div 2) <= d - e by ;
then A14: - (((p -' 1) div 2) - 1) <= d - e ;
A15: d <= (p -' 1) div 2 by ;
then d + e <= ((p -' 1) div 2) + ((p -' 1) div 2) by ;
then d + e < p by ;
then d + e,p are_coprime by ;
then A16: (d + e) gcd p = 1 by INT_2:def 3;
assume fp . d,fp . e are_congruent_mod p ; :: thesis: contradiction
then p divides (d ^2) - (fp . e) by A1, A7;
then p divides (d ^2) - (e ^2) by A1, A8;
then A17: p divides (d - e) * (d + e) ;
d - e <> 0 by A9;
then |.p.| <= |.(d - e).| by ;
then A18: p <= |.(d - e).| by ABSVALUE:def 1;
e >= 1 by ;
then d - e <= ((p -' 1) div 2) - 1 by ;
then |.(d - e).| <= ((p -' 1) div 2) - 1 by ;
hence contradiction by A18, A6, XXREAL_0:2; :: thesis: verum
end;
A19: for d being Nat st d in dom fp holds
d gcd p = 1
proof
let d be Nat; :: thesis: ( d in dom fp implies d gcd p = 1 )
A20: 1 * d <= 2 * d by XREAL_1:64;
assume d in dom fp ; :: thesis: d gcd p = 1
then A21: d in Seg ((p -' 1) div 2) by ;
then d <= (p -' 1) div 2 by FINSEQ_1:1;
then 2 * d <= ((p -' 1) / 2) * 2 by ;
then d <= p -' 1 by ;
then A22: d < p by ;
d >= 1 by ;
then d,p are_coprime by ;
hence d gcd p = 1 by INT_2:def 3; :: thesis: verum
end;
A23: for d being Nat st d in dom fp holds
(fp . d) gcd p = 1
proof
let d be Nat; :: thesis: ( d in dom fp implies (fp . d) gcd p = 1 )
assume A24: d in dom fp ; :: thesis: (fp . d) gcd p = 1
then d gcd p = 1 by A19;
then (d ^2) gcd p = 1 by WSIERP_1:7;
hence (fp . d) gcd p = 1 by ; :: thesis: verum
end;
take fp ; :: thesis: ( len fp = (p -' 1) div 2 & ( for d being Nat st d in dom fp holds
(fp . d) gcd p = 1 ) & ( for d being Nat st d in dom fp holds
fp . d is_quadratic_residue_mod p ) & ( for d, e being Nat st d in dom fp & e in dom fp & d <> e holds
not fp . d,fp . e are_congruent_mod p ) )

for d being Nat st d in dom fp holds