let a be Integer; :: thesis: for m being Nat st a gcd m = 1 holds
a ^2 is_quadratic_residue_mod m
let m be Nat; :: thesis: ( a gcd m = 1 implies a ^2 is_quadratic_residue_mod m )
assume a gcd m = 1 ; :: 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