theorem Th11: :: EC_PF_1:11

for p being Prime holds 0 = 0. (GF p) by NAT_1:44, SUBSET_1:def 8;