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 that
A1: seq is bounded and
A2: 0 <= r ; :: thesis: lim_sup (r (#) seq) = r * (lim_sup seq)
superior_realsequence seq in Funcs (NAT,REAL) by FUNCT_2:8;
then A3: 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:4;
then reconsider X1 = rng (superior_realsequence seq) as non empty Subset of REAL by A3;

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

let n be Element of NAT ; :: thesis: (superior_realsequence (r (#) seq)) . n = (r (#) (superior_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_above by RINFSUP1:5;
(superior_realsequence (r (#) seq)) . n = upper_bound ((r (#) seq) ^\ n) by RINFSUP1:37
.= upper_bound (r (#) (seq ^\ n)) by SEQM_3:21
.= upper_bound (r ** Y1) by INTEGRA2:17
.= r * (upper_bound (seq ^\ n)) by A2, A6, INTEGRA2:13
.= r * ((superior_realsequence seq) . n) by RINFSUP1:37 ;
hence (superior_realsequence (r (#) seq)) . n = (r (#) (superior_realsequence seq)) . n by SEQ_1:9; :: thesis: verum

end;

then superior_realsequence (r (#) seq) = r (#) (superior_realsequence seq) by FUNCT_2:63;
then A7: rng (superior_realsequence (r (#) seq)) = r ** X1 by INTEGRA2:17;
superior_realsequence seq is bounded by A1, RINFSUP1:56;
then X1 is bounded_below by RINFSUP1:6;
hence lim_sup (r (#) seq) = r * (lim_sup seq) by A2, A7, INTEGRA2:15; :: thesis: verum