:: deftheorem defines * LOPBAN_3:def 6 :
for X being non empty multMagma
for S being sequence of X
for a being Element of X
for b₄ being sequence of X holds
( b₄ = S * a iff for n being Nat holds b₄ . n = (S . n) * a );