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