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_1:73;
hence a ^2 is_quadratic_residue_mod m ; :: thesis: verum