let a be Integer; :: thesis: for p being Prime holds Lege ((a ^2),p) = 1
let p be Prime; :: thesis: Lege ((a ^2),p) = 1
a ^2 is_quadratic_residue_mod p by Th9;
hence Lege ((a ^2),p) = 1 by Def3; :: thesis: verum