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

now :: thesis: sup (rng K) = c * (sup (rng L))

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 c * (sup (rng L)) <= y

proof

let y be UpperBound of rng K; :: thesis: 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: 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 c * (sup (rng L)) <= y by A8, A9; :: thesis: verum

end;

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

now :: thesis: for x being ExtReal st x in rng L holds
x <= y / c

let x be ExtReal; :: thesis: ( x in rng L implies x <= y / c )
assume x in rng L ; :: thesis: x <= y / c
then consider n being object 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 = c * (L . n) by A3;
then (c * (L . n)) / c <= y / c by A1, A10, A13, XXREAL_2:def 1, XXREAL_3:79;
hence x <= y / c by A10, A12, XXREAL_3:88; :: thesis: verum

end;

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

A15: now :: thesis: not y = -infty

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: 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;
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: c * (sup (rng L)) <= y

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

end;

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

then reconsider ry = y as Real ;
reconsider sl = sup (rng L) as Real by A4;
y / c = ry / c ;
then sl * c <= ry by A1, A10, A14, XREAL_1:83;
hence c * (sup (rng L)) <= y ; :: thesis: verum

end;

end;

end;

end;

end;

now :: thesis: for x being ExtReal st x in rng K holds
x <= c * (sup (rng L))

let x be ExtReal; :: thesis: ( x in rng K implies x <= 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 <= c * (sup (rng L))
then consider m being object 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 = c * (L . m) by A3, A21;
hence x <= c * (sup (rng L)) by A1, A22, XXREAL_3:71; :: thesis: verum

end;

then 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 :: thesis: for n being Nat holds K . n = 0

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 Th60;
hence sup (rng K) = c * (sup (rng L)) by A24, A25, Th60; :: thesis: verum

end;

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

now :: thesis: for n being object holds -infty < K . n

let n be object ; :: thesis: -infty < K . b₁
-infty < L . n by A2;
then A27: -infty * c < 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 * 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 () ;

A29: now :: thesis: for k being Real st 0 < k holds
ex n being Nat st not K . n <= k

let k be Real; :: thesis: ( 0 < k implies ex n being Nat st not K . n <= k )
reconsider k1 = k as Real ;
A30: (k / c) * c = (k1 / c) * c
.= 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: k / c < L . n by A1, A2, A23, A26, Th59;
(k / c) * c < c * (L . n) by A1, A26, A31, XXREAL_3:72;
then k < K . n by A3, A30;
hence not for n being Nat holds K . n <= k ; :: thesis: verum

end;

c * (sup (rng L)) = +infty by A1, A23, A26, XXREAL_3:def 5;
hence sup (rng K) = c * (sup (rng L)) by A28, A29, Th59; :: thesis: verum

end;

end;

end;

end;

end;

hence sup (rng K) = c * (sup (rng L)) ; :: thesis: K is ()

now :: thesis: for n being object holds -infty < K . n

let n be object ; :: thesis: -infty < K . b₁
A32: ( L . n = +infty implies c * (L . n) <> -infty ) by A1;
-infty < L . n by A2;
then A33: -infty <> 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 () ; :: thesis: verum