:: deftheorem defines * LOPBAN_3:def 7 :
for X being non empty multMagma
for seq1, seq2, b₄ being sequence of X holds
( b₄ = seq1 * seq2 iff for n being Nat holds b₄ . n = (seq1 . n) * (seq2 . n) );