:: deftheorem defra defines ren_add FIELD_5:def 6 :
for F being Field
for Z being set
for r being Renaming of the carrier of F,Z
for b₄ being BinOp of (rng r) holds
( b₄ = ren_add r iff for a, b being Element of rng r holds b₄ . (a,b) = r . (((r ") . a) + ((r ") . b)) );