theorem Th80: :: RINFSUP1:80

for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is bounded_above & seq1 is nonnegative & seq2 is bounded_above & seq2 is nonnegative holds
(superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n)