theorem Th8: :: SEQ_1:8

for seq, seq1, seq2 being Real_Sequence holds
( seq = seq1 (#) seq2 iff for n being Nat holds seq . n = (seq1 . n) * (seq2 . n) )