theorem :: RINFSUP1:78

for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is bounded_below & seq1 is nonnegative & seq2 is bounded_below & seq2 is nonnegative holds
(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)