:: deftheorem Def23 defines Int-mult-left ZMODUL01:def 20 :
for AG being non empty addLoopStr
for b₂ being Function of [: the carrier of INT.Ring, the carrier of AG:], the carrier of AG holds
( b₂ = Int-mult-left AG iff for i being Element of INT.Ring
for a being Element of AG holds
( ( i >= 0 implies b₂ . (i,a) = (Nat-mult-left AG) . (i,a) ) & ( i < 0 implies b₂ . (i,a) = (Nat-mult-left AG) . ((- i),(- a)) ) ) );