let seq be Real_Sequence; :: thesis: for r being Real st seq is bounded & 0 <= r holds
lim_inf (r (#) seq) = r * (lim_inf seq)
let r be Real; :: thesis: ( seq is bounded & 0 <= r implies lim_inf (r (#) seq) = r * (lim_inf seq) )
assume that
A1: seq is bounded and
A2: 0 <= r ; :: thesis: lim_inf (r (#) seq) = r * (lim_inf seq)
inferior_realsequence seq in Funcs (NAT,REAL) by FUNCT_2:8;
then A3: ex f being Function st
( inferior_realsequence seq = f & dom f = NAT & rng f c= REAL ) by FUNCT_2:def 2;
(inferior_realsequence seq) . 0 in rng (inferior_realsequence seq) by FUNCT_2:4;
then reconsider X1 = rng (inferior_realsequence seq) as non empty Subset of REAL by A3;

now :: thesis: for n being Element of NAT holds (inferior_realsequence (r (#) seq)) . n = (r (#) (inferior_realsequence seq)) . n

let n be Element of NAT ; :: thesis: (inferior_realsequence (r (#) seq)) . n = (r (#) (inferior_realsequence seq)) . n
consider r1 being Real such that
A4: 0 < r1 and
A5: for k being Nat holds |.(seq . k).| < r1 by A1, SEQ_2:3;
seq ^\ n in Funcs (NAT,REAL) by FUNCT_2:8;
then ex f being Function st
( seq ^\ n = f & dom f = NAT & rng f c= REAL ) by FUNCT_2:def 2;
then reconsider Y1 = rng (seq ^\ n) as non empty Subset of REAL by FUNCT_2:4;

now :: thesis: for k being Nat holds |.((seq ^\ n) . k).| < r1

let k be Nat; :: thesis: |.((seq ^\ n) . k).| < r1
|.((seq ^\ n) . k).| = |.(seq . (n + k)).| by NAT_1:def 3;
hence |.((seq ^\ n) . k).| < r1 by A5; :: thesis: verum

end;

then seq ^\ n is bounded by A4, SEQ_2:3;
then A6: Y1 is bounded_below by RINFSUP1:6;
(inferior_realsequence (r (#) seq)) . n = lower_bound ((r (#) seq) ^\ n) by RINFSUP1:36
.= lower_bound (r (#) (seq ^\ n)) by SEQM_3:21
.= lower_bound (r ** Y1) by INTEGRA2:17
.= r * (lower_bound (seq ^\ n)) by A2, A6, INTEGRA2:15
.= r * ((inferior_realsequence seq) . n) by RINFSUP1:36 ;
hence (inferior_realsequence (r (#) seq)) . n = (r (#) (inferior_realsequence seq)) . n by SEQ_1:9; :: thesis: verum

end;

then inferior_realsequence (r (#) seq) = r (#) (inferior_realsequence seq) by FUNCT_2:63;
then A7: rng (inferior_realsequence (r (#) seq)) = r ** X1 by INTEGRA2:17;
inferior_realsequence seq is bounded by A1, RINFSUP1:56;
then X1 is bounded_above by RINFSUP1:5;
hence lim_inf (r (#) seq) = r * (lim_inf seq) by A2, A7, INTEGRA2:13; :: thesis: verum