:: deftheorem defrm defines ren_mult FIELD_5:def 7 :
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_mult r iff for a, b being Element of rng r holds b₄ . (a,b) = r . (((r ") . a) * ((r ") . b)) );