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