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 () )

( 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))end;

hence
sup (rng K) = c * (sup (rng L))
; :: thesis: K is ()per cases
( sup (rng L) in REAL or sup (rng L) = +infty )
by A2, Lm8;

end;

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

hence sup (rng K) = c * (sup (rng L)) by A5, XXREAL_2:def 3; :: thesis: verum

end;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;

end;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 )
;

end;

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;K . 1 = c * (L . 1) by A3;

hence c * (sup (rng L)) <= y by A8, A9; :: thesis: verum

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

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

end;

now :: thesis: for x being ExtReal st x in rng L holds

x <= y / c

then
y / c is UpperBound of rng L
by XXREAL_2:def 1;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;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

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;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

now :: thesis: for x being ExtReal st x in rng K holds

x <= c * (sup (rng L))

then
c * (sup (rng L)) is UpperBound of rng K
by XXREAL_2:def 1;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;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

hence sup (rng K) = c * (sup (rng L)) by A5, XXREAL_2:def 3; :: thesis: verum

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

end;

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

end;

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

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

end;

A25: now :: thesis: for n being Nat holds K . n = 0

then
lim K = sup (rng K)
by Th60;let n be Nat; :: thesis: K . n = 0

K . n = c * (L . n) by A3;

hence K . n = 0 by A24; :: thesis: verum

end;K . n = c * (L . n) by A3;

hence K . n = 0 by A24; :: thesis: verum

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

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

hence sup (rng K) = c * (sup (rng L)) by A28, A29, Th59; :: thesis: verum

end;

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

then A28:
K is ()
;let n be object ; :: thesis: -infty < K . b_{1}

-infty < L . n by A2;

then A27: -infty * c < c * (L . n) by A1, A26, XXREAL_3:72;

end;-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 )
;

end;

suppose
n in dom K
; :: thesis: -infty < K . b_{1}

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;-infty * c = -infty by A1, A26, XXREAL_3:def 5;

then -infty < K . n1 by A3, A27;

hence -infty < K . n ; :: thesis: verum

A29: now :: thesis: for k being Real st 0 < k holds

ex n being Nat st not K . n <= k

c * (sup (rng L)) = +infty
by A1, A23, A26, XXREAL_3:def 5;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;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

hence sup (rng K) = c * (sup (rng L)) by A28, A29, Th59; :: thesis: verum

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

hence
K is ()
; :: thesis: verumlet n be object ; :: thesis: -infty < K . b_{1}

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;

end;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;