let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being Real st 0 <= c & ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

integral+ (M,(c (#) f)) = c * (integral+ (M,f))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being Real st 0 <= c & ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

integral+ (M,(c (#) f)) = c * (integral+ (M,f))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for c being Real st 0 <= c & ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

integral+ (M,(c (#) f)) = c * (integral+ (M,f))

let f be PartFunc of X,ExtREAL; :: thesis: for c being Real st 0 <= c & ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

integral+ (M,(c (#) f)) = c * (integral+ (M,f))

let c be Real; :: thesis: ( 0 <= c & ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative implies integral+ (M,(c (#) f)) = c * (integral+ (M,f)) )

assume that

A1: 0 <= c and

A2: ex A being Element of S st

( A = dom f & f is A -measurable ) and

A3: f is nonnegative ; :: thesis: integral+ (M,(c (#) f)) = c * (integral+ (M,f))

consider F1 being Functional_Sequence of X,ExtREAL, K1 being ExtREAL_sequence such that

A4: for n being Nat holds

( F1 . n is_simple_func_in S & dom (F1 . n) = dom f ) and

A5: for n being Nat holds F1 . n is nonnegative and

A6: for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F1 . n) . x <= (F1 . m) . x and

A7: for x being Element of X st x in dom f holds

( F1 # x is convergent & lim (F1 # x) = f . x ) and

A8: for n being Nat holds K1 . n = integral' (M,(F1 . n)) and

K1 is convergent and

A9: integral+ (M,f) = lim K1 by A2, A3, Def15;

deffunc H_{1}( Nat) -> Element of bool [:X,ExtREAL:] = c (#) (F1 . $1);

consider F being Functional_Sequence of X,ExtREAL such that

A10: for n being Nat holds F . n = H_{1}(n)
from SEQFUNC:sch 1();

A11: c (#) f is nonnegative by A1, A3, Th20;

A12: for n being Nat holds F . n is nonnegative

A13: A = dom f and

A14: f is A -measurable by A2;

A15: c (#) f is A -measurable by A13, A14, MESFUNC1:37;

A16: for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom (c (#) f) )

K1 . n <= K1 . m_{2}( Nat) -> Element of ExtREAL = integral' (M,(F . $1));

consider K being ExtREAL_sequence such that

A31: for n being Element of NAT holds K . n = H_{2}(n)
from FUNCT_2:sch 4();

A37: for x being Element of X st x in dom (c (#) f) holds

( F # x is convergent & lim (F # x) = (c (#) f) . x )

then A48: lim K = c * (lim K1) by A1, A18, A33, Th63;

A49: for n, m being Nat st n <= m holds

for x being Element of X st x in dom (c (#) f) holds

(F . n) . x <= (F . m) . x

hence integral+ (M,(c (#) f)) = c * (integral+ (M,f)) by A9, A36, A15, A11, A32, A16, A12, A49, A37, A48, Def15; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being Real st 0 <= c & ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

integral+ (M,(c (#) f)) = c * (integral+ (M,f))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being Real st 0 <= c & ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

integral+ (M,(c (#) f)) = c * (integral+ (M,f))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for c being Real st 0 <= c & ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

integral+ (M,(c (#) f)) = c * (integral+ (M,f))

let f be PartFunc of X,ExtREAL; :: thesis: for c being Real st 0 <= c & ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

integral+ (M,(c (#) f)) = c * (integral+ (M,f))

let c be Real; :: thesis: ( 0 <= c & ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative implies integral+ (M,(c (#) f)) = c * (integral+ (M,f)) )

assume that

A1: 0 <= c and

A2: ex A being Element of S st

( A = dom f & f is A -measurable ) and

A3: f is nonnegative ; :: thesis: integral+ (M,(c (#) f)) = c * (integral+ (M,f))

consider F1 being Functional_Sequence of X,ExtREAL, K1 being ExtREAL_sequence such that

A4: for n being Nat holds

( F1 . n is_simple_func_in S & dom (F1 . n) = dom f ) and

A5: for n being Nat holds F1 . n is nonnegative and

A6: for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F1 . n) . x <= (F1 . m) . x and

A7: for x being Element of X st x in dom f holds

( F1 # x is convergent & lim (F1 # x) = f . x ) and

A8: for n being Nat holds K1 . n = integral' (M,(F1 . n)) and

K1 is convergent and

A9: integral+ (M,f) = lim K1 by A2, A3, Def15;

deffunc H

consider F being Functional_Sequence of X,ExtREAL such that

A10: for n being Nat holds F . n = H

A11: c (#) f is nonnegative by A1, A3, Th20;

A12: for n being Nat holds F . n is nonnegative

proof

consider A being Element of S such that
let n be Nat; :: thesis: F . n is nonnegative

reconsider n = n as Element of NAT by ORDINAL1:def 12;

F1 . n is nonnegative by A5;

then c (#) (F1 . n) is nonnegative by A1, Th20;

hence F . n is nonnegative by A10; :: thesis: verum

end;reconsider n = n as Element of NAT by ORDINAL1:def 12;

F1 . n is nonnegative by A5;

then c (#) (F1 . n) is nonnegative by A1, Th20;

hence F . n is nonnegative by A10; :: thesis: verum

A13: A = dom f and

A14: f is A -measurable by A2;

A15: c (#) f is A -measurable by A13, A14, MESFUNC1:37;

A16: for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom (c (#) f) )

proof

A18:
for n, m being Nat st n <= m holds
let n be Nat; :: thesis: ( F . n is_simple_func_in S & dom (F . n) = dom (c (#) f) )

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A17: F . n1 = c (#) (F1 . n1) by A10;

hence F . n is_simple_func_in S by A4, Th39; :: thesis: dom (F . n) = dom (c (#) f)

thus dom (F . n) = dom (F1 . n) by A17, MESFUNC1:def 6

.= A by A4, A13

.= dom (c (#) f) by A13, MESFUNC1:def 6 ; :: thesis: verum

end;reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A17: F . n1 = c (#) (F1 . n1) by A10;

hence F . n is_simple_func_in S by A4, Th39; :: thesis: dom (F . n) = dom (c (#) f)

thus dom (F . n) = dom (F1 . n) by A17, MESFUNC1:def 6

.= A by A4, A13

.= dom (c (#) f) by A13, MESFUNC1:def 6 ; :: thesis: verum

K1 . n <= K1 . m

proof

deffunc H
let n, m be Nat; :: thesis: ( n <= m implies K1 . n <= K1 . m )

A19: K1 . n = integral' (M,(F1 . n)) by A8;

A20: K1 . m = integral' (M,(F1 . m)) by A8;

A21: F1 . m is_simple_func_in S by A4;

A22: F1 . n is nonnegative by A5;

A23: dom (F1 . n) = dom f by A4;

A24: F1 . m is nonnegative by A5;

A25: dom (F1 . m) = dom f by A4;

assume A26: n <= m ; :: thesis: K1 . n <= K1 . m

A27: for x being object st x in dom ((F1 . m) - (F1 . n)) holds

(F1 . n) . x <= (F1 . m) . x

then A29: dom ((F1 . m) - (F1 . n)) = (dom (F1 . m)) /\ (dom (F1 . n)) by A21, A22, A24, A27, Th69;

then A30: (F1 . m) | (dom ((F1 . m) - (F1 . n))) = F1 . m by A23, A25, GRFUNC_1:23;

(F1 . n) | (dom ((F1 . m) - (F1 . n))) = F1 . n by A23, A25, A29, GRFUNC_1:23;

hence K1 . n <= K1 . m by A19, A20, A28, A21, A22, A24, A27, A30, Th70; :: thesis: verum

end;A19: K1 . n = integral' (M,(F1 . n)) by A8;

A20: K1 . m = integral' (M,(F1 . m)) by A8;

A21: F1 . m is_simple_func_in S by A4;

A22: F1 . n is nonnegative by A5;

A23: dom (F1 . n) = dom f by A4;

A24: F1 . m is nonnegative by A5;

A25: dom (F1 . m) = dom f by A4;

assume A26: n <= m ; :: thesis: K1 . n <= K1 . m

A27: for x being object st x in dom ((F1 . m) - (F1 . n)) holds

(F1 . n) . x <= (F1 . m) . x

proof

A28:
F1 . n is_simple_func_in S
by A4;
let x be object ; :: thesis: ( x in dom ((F1 . m) - (F1 . n)) implies (F1 . n) . x <= (F1 . m) . x )

assume x in dom ((F1 . m) - (F1 . n)) ; :: thesis: (F1 . n) . x <= (F1 . m) . x

then x in ((dom (F1 . m)) /\ (dom (F1 . n))) \ ((((F1 . m) " {+infty}) /\ ((F1 . n) " {+infty})) \/ (((F1 . m) " {-infty}) /\ ((F1 . n) " {-infty}))) by MESFUNC1:def 4;

then x in (dom (F1 . m)) /\ (dom (F1 . n)) by XBOOLE_0:def 5;

hence (F1 . n) . x <= (F1 . m) . x by A6, A26, A23, A25; :: thesis: verum

end;assume x in dom ((F1 . m) - (F1 . n)) ; :: thesis: (F1 . n) . x <= (F1 . m) . x

then x in ((dom (F1 . m)) /\ (dom (F1 . n))) \ ((((F1 . m) " {+infty}) /\ ((F1 . n) " {+infty})) \/ (((F1 . m) " {-infty}) /\ ((F1 . n) " {-infty}))) by MESFUNC1:def 4;

then x in (dom (F1 . m)) /\ (dom (F1 . n)) by XBOOLE_0:def 5;

hence (F1 . n) . x <= (F1 . m) . x by A6, A26, A23, A25; :: thesis: verum

then A29: dom ((F1 . m) - (F1 . n)) = (dom (F1 . m)) /\ (dom (F1 . n)) by A21, A22, A24, A27, Th69;

then A30: (F1 . m) | (dom ((F1 . m) - (F1 . n))) = F1 . m by A23, A25, GRFUNC_1:23;

(F1 . n) | (dom ((F1 . m) - (F1 . n))) = F1 . n by A23, A25, A29, GRFUNC_1:23;

hence K1 . n <= K1 . m by A19, A20, A28, A21, A22, A24, A27, A30, Th70; :: thesis: verum

consider K being ExtREAL_sequence such that

A31: for n being Element of NAT holds K . n = H

A32: now :: thesis: for n being Nat holds K . n = H_{2}(n)

A33:
for n being Nat holds K . n = c * (K1 . n)
let n be Nat; :: thesis: K . n = H_{2}(n)

n in NAT by ORDINAL1:def 12;

hence K . n = H_{2}(n)
by A31; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence K . n = H

proof

A36:
A = dom (c (#) f)
by A13, MESFUNC1:def 6;
let n be Nat; :: thesis: K . n = c * (K1 . n)

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A34: F1 . n is_simple_func_in S by A4;

A35: F . n1 = c (#) (F1 . n1) by A10;

thus K . n = integral' (M,(F . n1)) by A32

.= c * (integral' (M,(F1 . n))) by A1, A5, A34, A35, Th66

.= c * (K1 . n) by A8 ; :: thesis: verum

end;reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A34: F1 . n is_simple_func_in S by A4;

A35: F . n1 = c (#) (F1 . n1) by A10;

thus K . n = integral' (M,(F . n1)) by A32

.= c * (integral' (M,(F1 . n))) by A1, A5, A34, A35, Th66

.= c * (K1 . n) by A8 ; :: thesis: verum

A37: for x being Element of X st x in dom (c (#) f) holds

( F # x is convergent & lim (F # x) = (c (#) f) . x )

proof

let x be Element of X; :: thesis: ( x in dom (c (#) f) implies ( F # x is convergent & lim (F # x) = (c (#) f) . x ) )

assume A40: x in dom (c (#) f) ; :: thesis: ( F # x is convergent & lim (F # x) = (c (#) f) . x )

.= (c (#) f) . x by A40, MESFUNC1:def 6 ;

hence ( F # x is convergent & lim (F # x) = (c (#) f) . x ) by A1, A41, A39, A43, Th63; :: thesis: verum

end;now :: thesis: for n1 being set st n1 in dom (F1 # x) holds

-infty < (F1 # x) . n1

then A39:
F1 # x is ()
by Th10;-infty < (F1 # x) . n1

let n1 be set ; :: thesis: ( n1 in dom (F1 # x) implies -infty < (F1 # x) . n1 )

assume n1 in dom (F1 # x) ; :: thesis: -infty < (F1 # x) . n1

then reconsider n = n1 as Element of NAT ;

A38: (F1 # x) . n = (F1 . n) . x by Def13;

F1 . n is nonnegative by A5;

hence -infty < (F1 # x) . n1 by A38, Def5; :: thesis: verum

end;assume n1 in dom (F1 # x) ; :: thesis: -infty < (F1 # x) . n1

then reconsider n = n1 as Element of NAT ;

A38: (F1 # x) . n = (F1 . n) . x by Def13;

F1 . n is nonnegative by A5;

hence -infty < (F1 # x) . n1 by A38, Def5; :: thesis: verum

assume A40: x in dom (c (#) f) ; :: thesis: ( F # x is convergent & lim (F # x) = (c (#) f) . x )

A41: now :: thesis: for n being Nat holds (F # x) . n = c * ((F1 # x) . n)

let n be Nat; :: thesis: (F # x) . n = c * ((F1 # x) . n)

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A42: dom (c (#) (F1 . n1)) = dom (F . n1) by A10

.= dom (c (#) f) by A16 ;

thus (F # x) . n = (F . n) . x by Def13

.= (c (#) (F1 . n1)) . x by A10

.= c * ((F1 . n) . x) by A40, A42, MESFUNC1:def 6

.= c * ((F1 # x) . n) by Def13 ; :: thesis: verum

end;reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

A42: dom (c (#) (F1 . n1)) = dom (F . n1) by A10

.= dom (c (#) f) by A16 ;

thus (F # x) . n = (F . n) . x by Def13

.= (c (#) (F1 . n1)) . x by A10

.= c * ((F1 . n) . x) by A40, A42, MESFUNC1:def 6

.= c * ((F1 # x) . n) by Def13 ; :: thesis: verum

A43: now :: thesis: for n, m being Nat st n <= m holds

(F1 # x) . n <= (F1 # x) . m

c * (lim (F1 # x)) =
c * (f . x)
by A7, A13, A36, A40
(F1 # x) . n <= (F1 # x) . m

let n, m be Nat; :: thesis: ( n <= m implies (F1 # x) . n <= (F1 # x) . m )

assume A44: n <= m ; :: thesis: (F1 # x) . n <= (F1 # x) . m

A45: (F1 # x) . m = (F1 . m) . x by Def13;

(F1 # x) . n = (F1 . n) . x by Def13;

hence (F1 # x) . n <= (F1 # x) . m by A6, A13, A36, A40, A44, A45; :: thesis: verum

end;assume A44: n <= m ; :: thesis: (F1 # x) . n <= (F1 # x) . m

A45: (F1 # x) . m = (F1 . m) . x by Def13;

(F1 # x) . n = (F1 . n) . x by Def13;

hence (F1 # x) . n <= (F1 # x) . m by A6, A13, A36, A40, A44, A45; :: thesis: verum

.= (c (#) f) . x by A40, MESFUNC1:def 6 ;

hence ( F # x is convergent & lim (F # x) = (c (#) f) . x ) by A1, A41, A39, A43, Th63; :: thesis: verum

now :: thesis: for n1 being set st n1 in dom K1 holds

-infty < K1 . n1

then A47:
K1 is ()
by Th10;-infty < K1 . n1

let n1 be set ; :: thesis: ( n1 in dom K1 implies -infty < K1 . n1 )

assume n1 in dom K1 ; :: thesis: -infty < K1 . n1

then reconsider n = n1 as Element of NAT ;

A46: F1 . n is_simple_func_in S by A4;

K1 . n = integral' (M,(F1 . n)) by A8;

hence -infty < K1 . n1 by A5, A46, Th68; :: thesis: verum

end;assume n1 in dom K1 ; :: thesis: -infty < K1 . n1

then reconsider n = n1 as Element of NAT ;

A46: F1 . n is_simple_func_in S by A4;

K1 . n = integral' (M,(F1 . n)) by A8;

hence -infty < K1 . n1 by A5, A46, Th68; :: thesis: verum

then A48: lim K = c * (lim K1) by A1, A18, A33, Th63;

A49: for n, m being Nat st n <= m holds

for x being Element of X st x in dom (c (#) f) holds

(F . n) . x <= (F . m) . x

proof

K is convergent
by A1, A47, A18, A33, Th63;
let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X st x in dom (c (#) f) holds

(F . n) . x <= (F . m) . x )

assume A50: n <= m ; :: thesis: for x being Element of X st x in dom (c (#) f) holds

(F . n) . x <= (F . m) . x

reconsider n = n, m = m as Element of NAT by ORDINAL1:def 12;

let x be Element of X; :: thesis: ( x in dom (c (#) f) implies (F . n) . x <= (F . m) . x )

assume A51: x in dom (c (#) f) ; :: thesis: (F . n) . x <= (F . m) . x

dom (c (#) (F1 . m)) = dom (F . m) by A10;

then A52: dom (c (#) (F1 . m)) = dom (c (#) f) by A16;

(F . m) . x = (c (#) (F1 . m)) . x by A10;

then A53: (F . m) . x = c * ((F1 . m) . x) by A51, A52, MESFUNC1:def 6;

dom (c (#) (F1 . n)) = dom (F . n) by A10;

then A54: dom (c (#) (F1 . n)) = dom (c (#) f) by A16;

(F . n) . x = (c (#) (F1 . n)) . x by A10;

then (F . n) . x = c * ((F1 . n) . x) by A51, A54, MESFUNC1:def 6;

hence (F . n) . x <= (F . m) . x by A1, A6, A13, A36, A50, A51, A53, XXREAL_3:71; :: thesis: verum

end;(F . n) . x <= (F . m) . x )

assume A50: n <= m ; :: thesis: for x being Element of X st x in dom (c (#) f) holds

(F . n) . x <= (F . m) . x

reconsider n = n, m = m as Element of NAT by ORDINAL1:def 12;

let x be Element of X; :: thesis: ( x in dom (c (#) f) implies (F . n) . x <= (F . m) . x )

assume A51: x in dom (c (#) f) ; :: thesis: (F . n) . x <= (F . m) . x

dom (c (#) (F1 . m)) = dom (F . m) by A10;

then A52: dom (c (#) (F1 . m)) = dom (c (#) f) by A16;

(F . m) . x = (c (#) (F1 . m)) . x by A10;

then A53: (F . m) . x = c * ((F1 . m) . x) by A51, A52, MESFUNC1:def 6;

dom (c (#) (F1 . n)) = dom (F . n) by A10;

then A54: dom (c (#) (F1 . n)) = dom (c (#) f) by A16;

(F . n) . x = (c (#) (F1 . n)) . x by A10;

then (F . n) . x = c * ((F1 . n) . x) by A51, A54, MESFUNC1:def 6;

hence (F . n) . x <= (F . m) . x by A1, A6, A13, A36, A50, A51, A53, XXREAL_3:71; :: thesis: verum

hence integral+ (M,(c (#) f)) = c * (integral+ (M,f)) by A9, A36, A15, A11, A32, A16, A12, A49, A37, A48, Def15; :: thesis: verum