let p be Prime; :: thesis: for a being Element of (GF p) st a <> 0 holds
Lege_p (a |^ 2) = 1
let a be Element of (GF p); :: thesis: ( a <> 0 implies Lege_p (a |^ 2) = 1 )
assume a <> 0 ; :: thesis: Lege_p (a |^ 2) = 1
then a |^ 2 is quadratic_residue by QR1;
hence Lege_p (a |^ 2) = 1 by QR11; :: thesis: verum