let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded_below & seq1 is nonnegative & seq2 is bounded_below & seq2 is nonnegative implies ( seq1 (#) seq2 is bounded_below & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) ) )
assume that
A1: ( seq1 is bounded_below & seq1 is nonnegative ) and
A2: ( seq2 is bounded_below & seq2 is nonnegative ) ; :: thesis: ( seq1 (#) seq2 is bounded_below & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) )
for n being Nat holds (seq1 (#) seq2) . n >= (lower_bound seq1) * (lower_bound seq2)

proof

let n be Nat; :: thesis: (seq1 (#) seq2) . n >= (lower_bound seq1) * (lower_bound seq2)
A3: ( (seq1 (#) seq2) . n = (seq1 . n) * (seq2 . n) & seq1 . n >= lower_bound seq1 ) by A1, Th8, SEQ_1:8;
A4: lower_bound seq2 >= 0 by A2, Th18;
( seq2 . n >= lower_bound seq2 & lower_bound seq1 >= 0 ) by A1, A2, Th8, Th18;
hence (seq1 (#) seq2) . n >= (lower_bound seq1) * (lower_bound seq2) by A3, A4, XREAL_1:66; :: thesis: verum

end;

hence ( seq1 (#) seq2 is bounded_below & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) ) by Th10; :: thesis: verum