theorem Th4: :: TOPRNS_1:4

for N, n being Nat
for seq1, seq2 being Real_Sequence of N holds (seq1 + seq2) . n = (seq1 . n) + (seq2 . n)