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