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 A4: sup (rng L) in REAL ; :: thesis: sup (rng K) = c * (sup (rng L))

A5: 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;
A6: dom L = NAT by FUNCT_2:def 1;
A7: dom K = NAT by FUNCT_2:def 1;

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

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

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

end;

suppose A10: 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
A11: n in dom L and
A12: x = L . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A11;
A13: K . n in rng K by A7, FUNCT_1:3;
K . n = (R_EAL c) * (L . n) by A3;
then ((R_EAL c) * (L . n)) / (R_EAL c) <= y / (R_EAL c) by A1, A10, A13, XXREAL_2:def 1, XXREAL_3:79;
hence x <= y / (R_EAL c) by A10, A12, XXREAL_3:88; :: thesis: verum

end;

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

A15: now

assume A16: y = -infty ; :: thesis: contradiction
K . 1 in rng K by A7, FUNCT_1:3;
then K . 1 = -infty by A16, XXREAL_0:6, XXREAL_2:def 1;
then A17: (R_EAL c) * (L . 1) = -infty by A3;
L . 1 <= sup (rng L) by A6, FUNCT_1:3, XXREAL_2:4;
then A18: L . 1 < +infty by A4, XXREAL_0:2, XXREAL_0:9;
-infty < L . 1 by A2, Def5;
hence contradiction by A17, A18, XXREAL_3:70; :: thesis: verum

end;

per cases ( y = +infty or y in REAL ) by A15, 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 A4;
y / (R_EAL c) = ry / c by EXTREAL1:2;
then sl * c <= ry by A1, A10, A14, XREAL_1:83;
hence (R_EAL c) * (sup (rng L)) <= y by EXTREAL1:1; :: 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)) )
A19: 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
A20: m in dom K and
A21: x = K . m by FUNCT_1:def 3;
reconsider m = m as Element of NAT by A20;
dom L = NAT by FUNCT_2:def 1;
then A22: L . m <= sup (rng L) by A19, FUNCT_1:3, XXREAL_2:def 1;
x = (R_EAL c) * (L . m) by A3, A21;
hence x <= (R_EAL c) * (sup (rng L)) by A1, A22, XXREAL_3:71; :: 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 A5, XXREAL_2:def 3; :: thesis: verum

end;

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

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

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

A25: now

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

end;

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

end;

suppose A26: 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 A27: -infty * (R_EAL c) < (R_EAL c) * (L . n) by A1, A26, XXREAL_3:72;

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, A26, XXREAL_3:def 5;
then -infty < K . n1 by A3, A27;
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 2; :: thesis: verum

end;

end;

end;

then A28: K is without-infty by Def5;

A29: 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;
A30: (R_EAL (k / c)) * (R_EAL c) = (k1 / c) * c by EXTREAL1:1
.= k1 / (c / c) by XCMPLX_1:82
.= k by A26, XCMPLX_1:51 ;
assume 0 < k ; :: thesis: not for n being Nat holds K . n <= k
then consider n being Nat such that
A31: R_EAL (k / c) < L . n by A1, A2, A23, A26, Th65;
(R_EAL (k / c)) * (R_EAL c) < (R_EAL c) * (L . n) by A1, A26, A31, XXREAL_3:72;
then R_EAL k < K . n by A3, A30;
hence not for n being Nat holds K . n <= k ; :: thesis: verum

end;

(R_EAL c) * (sup (rng L)) = +infty by A1, A23, A26, XXREAL_3:def 5;
hence sup (rng K) = c * (sup (rng L)) by A28, A29, 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₁
A32: ( L . n = +infty implies (R_EAL c) * (L . n) <> -infty ) by A1;
-infty < L . n by A2, Def5;
then A33: -infty <> (R_EAL c) * (L . n) by A32, XXREAL_3:70;

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, A33;
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 2; :: thesis: verum

end;

end;

end;

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