let n be Nat; :: thesis: for seq1, seq2 being Real_Sequence st seq1 is bounded_below & seq1 is nonnegative & seq2 is bounded_below & seq2 is nonnegative holds
(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)
let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded_below & seq1 is nonnegative & seq2 is bounded_below & seq2 is nonnegative implies (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) )
assume ( seq1 is bounded_below & seq1 is nonnegative & seq2 is bounded_below & seq2 is nonnegative ) ; :: thesis: (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)
then ( seq1 ^\ n is bounded_below & seq1 ^\ n is nonnegative & seq2 ^\ n is bounded_below & seq2 ^\ n is nonnegative ) by Th17, SEQM_3:28;
then lower_bound ((seq1 ^\ n) (#) (seq2 ^\ n)) >= (lower_bound (seq1 ^\ n)) * (lower_bound (seq2 ^\ n)) by Th20;
then A1: lower_bound ((seq1 (#) seq2) ^\ n) >= (lower_bound (seq1 ^\ n)) * (lower_bound (seq2 ^\ n)) by SEQM_3:19;
( (inferior_realsequence seq1) . n = lower_bound (seq1 ^\ n) & (inferior_realsequence seq2) . n = lower_bound (seq2 ^\ n) ) by Th36;
hence (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) by A1, Th36; :: thesis: verum