let a be Integer; :: thesis: for m being Nat holds a ^2 is_quadratic_residue_mod m
let m be Nat; :: thesis: a ^2 is_quadratic_residue_mod m
((a ^2) - (a ^2)) mod m = 0 by INT_4:12;
hence a ^2 is_quadratic_residue_mod m by Def2; :: thesis: verum