theorem Th12: :: EC_PF_1:12

for p being Prime holds 1 = 1. (GF p)