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 A1: a <> 0 ; :: thesis: a |^ 2 is quadratic_residue
reconsider b = a |^ 2 as Element of (GF p) ;
b <> 0 by A1, Th25;
hence a |^ 2 is quadratic_residue by Def3; :: thesis: verum