theorem Th12: :: EC_PF_1:12
for p being Prime holds 1 = 1. (GF p)