let n be Nat; :: thesis: 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)
let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded_above & seq1 is nonnegative & seq2 is bounded_above & seq2 is nonnegative implies (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n) )
assume ( seq1 is bounded_above & seq1 is nonnegative & seq2 is bounded_above & seq2 is nonnegative ) ; :: thesis: (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n)
then ( seq1 ^\ n is bounded_above & seq1 ^\ n is nonnegative & seq2 ^\ n is bounded_above & seq2 ^\ n is nonnegative ) by Th17, SEQM_3:27;
then upper_bound ((seq1 ^\ n) (#) (seq2 ^\ n)) <= (upper_bound (seq1 ^\ n)) * (upper_bound (seq2 ^\ n)) by Th21;
then A1: upper_bound ((seq1 (#) seq2) ^\ n) <= (upper_bound (seq1 ^\ n)) * (upper_bound (seq2 ^\ n)) by SEQM_3:19;
( (superior_realsequence seq1) . n = upper_bound (seq1 ^\ n) & (superior_realsequence seq2) . n = upper_bound (seq2 ^\ n) ) by Th37;
hence (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n) by A1, Th37; :: thesis: verum