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_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 A2: ( seq1 is bounded & seq1 is nonnegative & 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);
A4: ( inferior_realsequence seq1 is bounded & inferior_realsequence seq2 is bounded & inferior_realsequence seq1 is convergent & inferior_realsequence seq2 is convergent ) by A2, Th58, Th59;
then A5: (inferior_realsequence seq1) (#) (inferior_realsequence seq2) is convergent by SEQ_2:28;
seq1 (#) seq2 is bounded by A2;
then A7: ( inferior_realsequence (seq1 (#) seq2) is bounded & inferior_realsequence (seq1 (#) seq2) is convergent ) by Th58, Th59;
for n being Element of NAT holds (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) . n

proof

let n be Element of 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 A2, Th81;
hence (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) . n by SEQ_1:12; :: thesis: verum

end;

then A8: lim (inferior_realsequence (seq1 (#) seq2)) >= lim ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) by A5, A7, SEQ_2:32;
( sup (inferior_realsequence (seq1 (#) seq2)) = lim (inferior_realsequence (seq1 (#) seq2)) & sup (inferior_realsequence seq1) = lim (inferior_realsequence seq1) & sup (inferior_realsequence seq2) = lim (inferior_realsequence seq2) ) by A2, Th59;
hence (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) by A4, A8, SEQ_2:29; :: thesis: verum

end;

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 A9: ( seq1 is bounded & seq1 is nonnegative & 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);
A11: ( superior_realsequence seq1 is bounded & superior_realsequence seq2 is bounded & superior_realsequence seq1 is convergent & superior_realsequence seq2 is convergent ) by A9, Th58, Th60;
then A12: (superior_realsequence seq1) (#) (superior_realsequence seq2) is convergent by SEQ_2:28;
seq1 (#) seq2 is bounded by A9;
then A14: ( superior_realsequence (seq1 (#) seq2) is bounded & superior_realsequence (seq1 (#) seq2) is convergent ) by Th58, Th60;
for n being Element of NAT holds (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) (#) (superior_realsequence seq2)) . n

proof

let n be Element of 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 A9, Th82;
hence (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) (#) (superior_realsequence seq2)) . n by SEQ_1:12; :: thesis: verum

end;

then A15: lim (superior_realsequence (seq1 (#) seq2)) <= lim ((superior_realsequence seq1) (#) (superior_realsequence seq2)) by A12, A14, SEQ_2:32;
( inf (superior_realsequence (seq1 (#) seq2)) = lim (superior_realsequence (seq1 (#) seq2)) & inf (superior_realsequence seq1) = lim (superior_realsequence seq1) & inf (superior_realsequence seq2) = lim (superior_realsequence seq2) ) by A9, Th60;
hence lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) by A11, A15, SEQ_2:29; :: 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