let L, K be ExtREAL_sequence; :: thesis: for c being Real st 0 <= c & L is without-infty & ( for n being Nat holds K . n = (R_EAL c) * (L . n) ) holds
( sup (rng K) = (R_EAL c) * (sup (rng L)) & K is without-infty )
let c be Real; :: thesis: ( 0 <= c & L is without-infty & ( for n being Nat holds K . n = (R_EAL c) * (L . n) ) implies ( sup (rng K) = (R_EAL c) * (sup (rng L)) & K is without-infty ) )
assume that
A1: 0 <= c and
A2: L is without-infty and
A3: for n being Nat holds K . n = (R_EAL c) * (L . n) ; :: thesis: ( sup (rng K) = (R_EAL c) * (sup (rng L)) & K is without-infty )

now

per cases ( sup (rng L) in REAL or sup (rng L) = +infty ) by A2, Lm8;

suppose A6: sup (rng L) in REAL ; :: thesis: sup (rng K) = c * (sup (rng L))

A7: for y being UpperBound of rng K holds (R_EAL c) * (sup (rng L)) <= y

proof

let y be UpperBound of rng K; :: thesis: (R_EAL c) * (sup (rng L)) <= y
reconsider y = y as R_eal by XXREAL_0:def 1;
A8: dom L = NAT by FUNCT_2:def 1;
A9: dom K = NAT by FUNCT_2:def 1;

per cases ( c = 0 or c <> 0 ) ;

suppose A10: c = 0 ; :: thesis: (R_EAL c) * (sup (rng L)) <= y

A11: K . 1 <= y by A9, FUNCT_1:12, XXREAL_2:def 1;
K . 1 = c * (L . 1) by A3;
hence (R_EAL c) * (sup (rng L)) <= y by A10, A11; :: thesis: verum

end;

suppose A12: c <> 0 ; :: thesis: (R_EAL c) * (sup (rng L)) <= y

now

let x be ext-real number ; :: thesis: ( x in rng L implies x <= y / (R_EAL c) )
assume x in rng L ; :: thesis: x <= y / (R_EAL c)
then consider n being set such that
A13: n in dom L and
A14: x = L . n by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A13;
A15: K . n in rng K by A9, FUNCT_1:12;
K . n = (R_EAL c) * (L . n) by A3;
then ((R_EAL c) * (L . n)) / (R_EAL c) <= y / (R_EAL c) by A1, A12, A15, XXREAL_2:def 1, XXREAL_3:90;
hence x <= y / (R_EAL c) by A12, A14, XXREAL_3:99; :: thesis: verum

end;

then y / (R_EAL c) is UpperBound of rng L by XXREAL_2:def 1;
then A16: sup (rng L) <= y / (R_EAL c) by XXREAL_2:def 3;

A17: now

assume A18: y = -infty ; :: thesis: contradiction
K . 1 in rng K by A9, FUNCT_1:12;
then K . 1 = -infty by A18, XXREAL_0:6, XXREAL_2:def 1;
then A19: (R_EAL c) * (L . 1) = -infty by A3;
L . 1 <= sup (rng L) by A8, FUNCT_1:12, XXREAL_2:4;
then A20: L . 1 < +infty by A6, XXREAL_0:2, XXREAL_0:9;
-infty < L . 1 by A2, Def5;
hence contradiction by A19, A20, XXREAL_3:81; :: thesis: verum

end;

per cases ( y = +infty or y in REAL ) by A17, XXREAL_0:14;

suppose y = +infty ; :: thesis: (R_EAL c) * (sup (rng L)) <= y

hence (R_EAL c) * (sup (rng L)) <= y by XXREAL_0:4; :: thesis: verum

end;

suppose y in REAL ; :: thesis: (R_EAL c) * (sup (rng L)) <= y

then reconsider ry = y as Real ;
reconsider sl = sup (rng L) as Real by A6;
y / (R_EAL c) = ry / c by EXTREAL1:32;
then sl * c <= ry by A1, A12, A16, XREAL_1:85;
hence (R_EAL c) * (sup (rng L)) <= y by EXTREAL1:13; :: thesis: verum

end;

end;

end;

end;

end;

now

let x be ext-real number ; :: thesis: ( x in rng K implies x <= (R_EAL c) * (sup (rng L)) )
A21: sup (rng L) is UpperBound of rng L by XXREAL_2:def 3;
assume x in rng K ; :: thesis: x <= (R_EAL c) * (sup (rng L))
then consider m being set such that
A22: m in dom K and
A23: x = K . m by FUNCT_1:def 5;
reconsider m = m as Element of NAT by A22;
dom L = NAT by FUNCT_2:def 1;
then A24: L . m <= sup (rng L) by A21, FUNCT_1:12, XXREAL_2:def 1;
x = (R_EAL c) * (L . m) by A3, A23;
hence x <= (R_EAL c) * (sup (rng L)) by A1, A24, XXREAL_3:82; :: thesis: verum

end;

then (R_EAL c) * (sup (rng L)) is UpperBound of rng K by XXREAL_2:def 1;
hence sup (rng K) = c * (sup (rng L)) by A7, XXREAL_2:def 3; :: thesis: verum

end;

suppose A25: sup (rng L) = +infty ; :: thesis: sup (rng K) = c * (sup (rng L))

per cases ( c = 0 or c <> 0 ) ;

suppose A26: c = 0 ; :: thesis: sup (rng K) = c * (sup (rng L))

A27: now

let n be Nat; :: thesis: K . n = 0
K . n = c * (L . n) by A3;
hence K . n = 0 by A26; :: thesis: verum

end;

then lim K = sup (rng K) by Th66;
hence sup (rng K) = c * (sup (rng L)) by A26, A27, Th66; :: thesis: verum

end;

suppose A28: c <> 0 ; :: thesis: sup (rng K) = c * (sup (rng L))

now

let n be set ; :: thesis: -infty < K . b₁
-infty < L . n by A2, Def5;
then A29: -infty * (R_EAL c) < (R_EAL c) * (L . n) by A1, A28, XXREAL_3:83;

per cases ( n in dom K or not n in dom K ) ;

suppose n in dom K ; :: thesis: -infty < K . b₁

then reconsider n1 = n as Element of NAT ;
-infty * (R_EAL c) = -infty by A1, A28, XXREAL_3:def 5;
then -infty < K . n1 by A3, A29;
hence -infty < K . n ; :: thesis: verum

end;

suppose not n in dom K ; :: thesis: -infty < K . b₁

hence -infty < K . n by FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

then A30: K is without-infty by Def5;

A31: now

let k be real number ; :: thesis: ( 0 < k implies ex n being Nat st not K . n <= k )
reconsider k1 = k as Real by XREAL_0:def 1;
A32: (R_EAL (k / c)) * (R_EAL c) = (k1 / c) * c by EXTREAL1:13
.= k1 / (c / c) by XCMPLX_1:83
.= k by A28, XCMPLX_1:51 ;
assume 0 < k ; :: thesis: not for n being Nat holds K . n <= k
then consider n being Nat such that
A33: R_EAL (k / c) < L . n by A1, A2, A25, A28, Th65;
(R_EAL (k / c)) * (R_EAL c) < (R_EAL c) * (L . n) by A1, A28, A33, XXREAL_3:83;
then R_EAL k < K . n by A3, A32;
hence not for n being Nat holds K . n <= k ; :: thesis: verum

end;

(R_EAL c) * (sup (rng L)) = +infty by A1, A25, A28, XXREAL_3:def 5;
hence sup (rng K) = c * (sup (rng L)) by A30, A31, Th65; :: thesis: verum

end;

end;

end;

end;

end;

hence sup (rng K) = (R_EAL c) * (sup (rng L)) ; :: thesis: K is without-infty

now

let n be set ; :: thesis: -infty < K . b₁
A34: ( L . n = +infty implies (R_EAL c) * (L . n) <> -infty ) by A1;
-infty < L . n by A2, Def5;
then A35: -infty <> (R_EAL c) * (L . n) by A34, XXREAL_3:81;

per cases ( n in dom K or not n in dom K ) ;

suppose n in dom K ; :: thesis: -infty < K . b₁

then reconsider n1 = n as Element of NAT ;
K . n1 <> -infty by A3, A35;
hence -infty < K . n by XXREAL_0:6; :: thesis: verum

end;

suppose not n in dom K ; :: thesis: -infty < K . b₁

hence -infty < K . n by FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence K is without-infty by Def5; :: thesis: verum