:: deftheorem defrf defines RenField FIELD_5:def 8 :
for F being Field
for Z being set
for r being Renaming of the carrier of F,Z
for b₄ being strict doubleLoopStr holds
( b₄ = RenField r iff ( the carrier of b₄ = rng r & the addF of b₄ = ren_add r & the multF of b₄ = ren_mult r & the OneF of b₄ = r . (1. F) & the ZeroF of b₄ = r . (0. F) ) );