let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies ( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) ) )
A1: for seq1, seq2 being Real_Sequence st seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative holds
lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2)

proof

let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) )
assume that
A2: ( seq1 is bounded & seq1 is nonnegative ) and
A3: ( seq2 is bounded & seq2 is nonnegative ) ; :: thesis: lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2)
set seq3 = superior_realsequence seq1;
set seq4 = superior_realsequence seq2;
set seq5 = superior_realsequence (seq1 (#) seq2);
A4: superior_realsequence (seq1 (#) seq2) is convergent by A2, A3, Th58;
A5: ( lower_bound (superior_realsequence (seq1 (#) seq2)) = lim (superior_realsequence (seq1 (#) seq2)) & lower_bound (superior_realsequence seq1) = lim (superior_realsequence seq1) ) by A2, A3, Th58;
A6: lower_bound (superior_realsequence seq2) = lim (superior_realsequence seq2) by A3, Th58;
A7: for n being Nat holds (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) (#) (superior_realsequence seq2)) . n

proof

let n be Nat; :: thesis: (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) (#) (superior_realsequence seq2)) . n
(superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n) by A2, A3, Th80;
hence (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) (#) (superior_realsequence seq2)) . n by SEQ_1:8; :: thesis: verum

end;

A8: ( superior_realsequence seq1 is convergent & superior_realsequence seq2 is convergent ) by A2, A3, Th58;
then (superior_realsequence seq1) (#) (superior_realsequence seq2) is convergent ;
then lim (superior_realsequence (seq1 (#) seq2)) <= lim ((superior_realsequence seq1) (#) (superior_realsequence seq2)) by A4, A7, SEQ_2:18;
hence lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) by A8, A5, A6, SEQ_2:15; :: thesis: verum

end;

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

proof

let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) )
assume that
A9: ( seq1 is bounded & seq1 is nonnegative ) and
A10: ( seq2 is bounded & seq2 is nonnegative ) ; :: thesis: (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2)
set seq3 = inferior_realsequence seq1;
set seq4 = inferior_realsequence seq2;
set seq5 = inferior_realsequence (seq1 (#) seq2);
A11: inferior_realsequence (seq1 (#) seq2) is convergent by A9, A10, Th57;
A12: ( upper_bound (inferior_realsequence (seq1 (#) seq2)) = lim (inferior_realsequence (seq1 (#) seq2)) & upper_bound (inferior_realsequence seq1) = lim (inferior_realsequence seq1) ) by A9, A10, Th57;
A13: upper_bound (inferior_realsequence seq2) = lim (inferior_realsequence seq2) by A10, Th57;
A14: for n being Nat holds (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) . n

proof

let n be Nat; :: thesis: (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) . n
(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) by A9, A10, Th79;
hence (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) . n by SEQ_1:8; :: thesis: verum

end;

A15: ( inferior_realsequence seq1 is convergent & inferior_realsequence seq2 is convergent ) by A9, A10, Th57;
then (inferior_realsequence seq1) (#) (inferior_realsequence seq2) is convergent ;
then lim (inferior_realsequence (seq1 (#) seq2)) >= lim ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) by A11, A14, SEQ_2:18;
hence (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) by A15, A12, A13, SEQ_2:15; :: thesis: verum

end;

hence ( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies ( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) ) ) by A1; :: thesis: verum