let p be Prime; :: thesis: for a being Element of (GF p) st a <> 0 holds
a |^ 2 is quadratic_residue
let a be Element of (GF p); :: thesis: ( a <> 0 implies a |^ 2 is quadratic_residue )
assume P0: a <> 0 ; :: thesis: a |^ 2 is quadratic_residue
reconsider b = a |^ 2 as Element of (GF p) ;
b <> 0 by P0, EX6;
hence a |^ 2 is quadratic_residue by QRDef1; :: thesis: verum