A1: p > 1 by INT_2:def 4;
reconsider a = 1. (GF p) as Element of (GF p) ;
A2: a = 1 by A1, INT_3:14;
a |^ 2 = (1. (GF p)) * (1. (GF p)) by Lm2
.= 1_ (GF p) ;
hence 1. (GF p) is quadratic_residue by A2; :: thesis: verum