theorem :: RINFSUP1:77

for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is V95() & seq2 is V95() holds
(superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n)