theorem Th49: :: NUMBER02:49

for a being Nat holds
( (a ^2) mod 7 = 0 or (a ^2) mod 7 = 1 or (a ^2) mod 7 = 2 or (a ^2) mod 7 = 4 )