let a be Integer; :: thesis:
let p be Prime; :: thesis:
assume that
A1: p > 2 and
A2: a gcd p = 1 ; :: thesis:
not p divides a by Lm3, A2;
then A3: a mod p <> 0 by INT_1:62;
A4: p > 1 by INT_2:def 4;
then - p < - 1 by XREAL_1:24;
then A5: (- 1) mod p = p + (- 1) by NAT_D:63;

suppose A6: a is_quadratic_residue_mod p ; :: thesis:

then (a |^ ((p -' 1) div 2)) mod p = 1 by A1, A2, Th17;
then (a |^ ((p -' 1) div 2)) mod p = 1 mod p by A4, NAT_D:14;
then (a |^ ((p -' 1) div 2)) mod p = (Lege (a,p)) mod p by A6, Def3, A3;
hence Lege (a,p),a |^ ((p -' 1) div 2) are_congruent_mod p by NAT_D:64; :: thesis:

end;

suppose A7: not a is_quadratic_residue_mod p ; :: thesis:

then (a |^ ((p -' 1) div 2)) mod p = p - 1 by A1, A2, Th19
.= (Lege (a,p)) mod p by A5, A7, Def3 ;
hence Lege (a,p),a |^ ((p -' 1) div 2) are_congruent_mod p by NAT_D:64; :: thesis:

end;

end;