let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded_above & seq1 is nonnegative & seq2 is bounded_above & seq2 is nonnegative implies ( seq1 (#) seq2 is bounded_above & sup (seq1 (#) seq2) <= (sup seq1) * (sup seq2) ) )
assume A1: ( seq1 is bounded_above & seq1 is nonnegative & seq2 is bounded_above & seq2 is nonnegative ) ; :: thesis: ( seq1 (#) seq2 is bounded_above & sup (seq1 (#) seq2) <= (sup seq1) * (sup seq2) )
for n being Element of NAT holds (seq1 (#) seq2) . n <= (sup seq1) * (sup seq2)

proof

let n be Element of NAT ; :: thesis: (seq1 (#) seq2) . n <= (sup seq1) * (sup seq2)
A2: (seq1 (#) seq2) . n = (seq1 . n) * (seq2 . n) by SEQ_1:12;
A3: ( seq1 . n <= sup seq1 & seq2 . n <= sup seq2 ) by A1, Th7;
( seq1 . n >= 0 & seq2 . n >= 0 ) by A1, Def3;
hence (seq1 (#) seq2) . n <= (sup seq1) * (sup seq2) by A2, A3, XREAL_1:68; :: thesis: verum

end;

hence ( seq1 (#) seq2 is bounded_above & sup (seq1 (#) seq2) <= (sup seq1) * (sup seq2) ) by Th9; :: thesis: verum