a mod 5 < 4 + 1 by NAT_D:1;
then a mod 5 <= 4 by NAT_1:13;
then not not a mod 5 = 0 & ... & not a mod 5 = 4 ;
then ( (a |^ 2) mod 5 = (0 |^ 2) mod 5 or (a |^ 2) mod 5 = (1 |^ 2) mod 5 or (a |^ 2) mod 5 = (2 |^ 2) mod 5 or (a |^ 2) mod 5 = (3 |^ 2) mod 5 or (a |^ 2) mod 5 = (4 |^ 2) mod 5 ) by GR_CY_3:30;
then A1: ( (a |^ 2) mod 5 = 0 mod 5 or (a |^ 2) mod 5 = 1 mod 5 or (a |^ 2) mod 5 = (2 * 2) mod 5 or (a |^ 2) mod 5 = (3 * 3) mod 5 or (a |^ 2) mod 5 = (4 * 4) mod 5 ) by NEWTON:81;
( 1 mod (1 + 4) = (1 * ((5 * 3) + 1)) mod 5 & (4 + 5) mod 5 = (4 + (5 mod 5)) mod 5 ) by NEWTON02:88;
then ( (a |^ 2) mod 5 = 0 * 0 or (a |^ 2) mod 5 = 1 * 1 or (a |^ 2) mod 5 = 2 * 2 ) by A1;
hence (a |^ 2) mod 5 is square ; :: thesis: verum