let p be Prime; :: thesis: for a being Element of (GF p) holds
( a is quadratic_residue iff Lege_p a = 1 )
let a be Element of (GF p); :: thesis: ( a is quadratic_residue iff Lege_p a = 1 )
thus ( a is quadratic_residue implies Lege_p a = 1 ) by QRDef3; :: thesis: ( Lege_p a = 1 implies a is quadratic_residue )
assume Lege_p a = 1 ; :: thesis: a is quadratic_residue
then ( a <> 0 & Lege_p a <> - 1 ) by QRDef3;
hence a is quadratic_residue by QRDef3; :: thesis: verum