:: deftheorem defines * LOPBAN_3:def 5 :
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₄ = a * S iff for n being Nat holds b₄ . n = a * (S . n) );