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:11;
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:6;
then reconsider X1 = rng (inferior_realsequence seq) as non empty Subset of REAL by A3;

now

let n be Element of NAT ; :: thesis: (inferior_realsequence (r (#) seq)) . n = (r (#) (inferior_realsequence seq)) . n
consider r1 being real number such that
A4: 0 < r1 and
A5: for k being Element of NAT holds abs (seq . k) < r1 by A1, SEQ_2:15;
seq ^\ n in Funcs (NAT,REAL) by FUNCT_2:11;
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:6;

now

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

end;

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

end;

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