theorem Th7: :: SEQ_1:7

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