:: deftheorem Def2 defines * NAT_3:def 2 :
for X being set
for b being real-valued ManySortedSet of X
for a being Nat
for b₄ being ManySortedSet of X holds
( b₄ = a * b iff for i being object holds b₄ . i = a * (b . i) );