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

now

let n be Element of NAT ; :: thesis: (superior_realsequence (r (#) seq)) . n = (r (#) (superior_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_above by RINFSUP1:5;
(superior_realsequence (r (#) seq)) . n = sup ((r (#) seq) ^\ n) by RINFSUP1:39
.= sup (r (#) (seq ^\ n)) by SEQM_3:44
.= sup (r ** Y1) by INTEGRA2:17
.= r * (sup (seq ^\ n)) by A1, A5, INTEGRA2:13
.= r * ((superior_realsequence seq) . n) by RINFSUP1:39 ;
hence (superior_realsequence (r (#) seq)) . n = (r (#) (superior_realsequence seq)) . n by SEQ_1:13; :: thesis: verum

end;

then superior_realsequence (r (#) seq) = r (#) (superior_realsequence seq) by FUNCT_2:113;
then rng (superior_realsequence (r (#) seq)) = r ** X1 by INTEGRA2:17;
hence lim_sup (r (#) seq) = r * (lim_sup seq) by A1, A3, INTEGRA2:15; :: thesis: verum