:: deftheorem Def10 defines PrimeField RING_3:def 10 :
for F being Field
for b₂ being strict doubleLoopStr holds
( b₂ = PrimeField F iff ( the carrier of b₂ = carrier/\ F & the addF of b₂ = the addF of F || (carrier/\ F) & the multF of b₂ = the multF of F || (carrier/\ F) & the OneF of b₂ = 1. F & the ZeroF of b₂ = 0. F ) );