theorem Th16: :: INT_5:16

for p being Prime st p > 2 holds
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 ) )