for seq1, seq2 being Real_Sequence st seq1 is V95() & seq1 is nonnegative & seq2 is V95() & seq2 is nonnegative holds
( seq1 (#) seq2 is V95() & upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) )