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 A1: ( seq is bounded & 0 <= r ) ; :: thesis: lim_inf (r (#) seq) = r * (lim_inf seq)
inferior_realsequence seq in Funcs NAT ,REAL by FUNCT_2:11;
then A2: 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 A2;
inferior_realsequence seq is bounded by A1, RINFSUP1:58;
then A3: X1 is bounded_above by RINFSUP1:5;

now

let n be Element of NAT ; :: thesis: (inferior_realsequence (r (#) seq)) . n = (r (#) (inferior_realsequence seq)) . n
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;
consider r1 being real number such that
A4: ( 0 < r1 & ( for k being Element of NAT holds abs (seq . k) < r1 ) ) by A1, SEQ_2:15;

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 A4; :: thesis: verum

end;

then seq ^\ n is bounded by A4, SEQ_2:15;
then A5: Y1 is bounded_below by RINFSUP1:6;
(inferior_realsequence (r (#) seq)) . n = inf ((r (#) seq) ^\ n) by RINFSUP1:38
.= inf (r (#) (seq ^\ n)) by SEQM_3:44
.= lower_bound (r ** Y1) by INTEGRA2:17
.= r * (inf (seq ^\ n)) by A1, A5, 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 rng (inferior_realsequence (r (#) seq)) = r ** X1 by INTEGRA2:17;
hence lim_inf (r (#) seq) = r * (lim_inf seq) by A1, A3, INTEGRA2:13; :: thesis: verum