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_measurable_on A ) & f is nonnegative holds
integral+ M,(c (#) f) = (R_EAL 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_measurable_on A ) & f is nonnegative holds
integral+ M,(c (#) f) = (R_EAL 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_measurable_on A ) & f is nonnegative holds
integral+ M,(c (#) f) = (R_EAL 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_measurable_on A ) & f is nonnegative holds
integral+ M,(c (#) f) = (R_EAL c) * (integral+ M,f)
let c be Real; :: thesis: ( 0 <= c & ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative implies integral+ M,(c (#) f) = (R_EAL c) * (integral+ M,f) )
assume A1: ( 0 <= c & ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative ) ; :: thesis: integral+ M,(c (#) f) = (R_EAL c) * (integral+ M,f)
consider F1 being Functional_Sequence of X,ExtREAL , K1 being ExtREAL_sequence such that
A2: ( ( for n being Nat holds
( F1 . n is_simple_func_in S & dom (F1 . n) = dom f ) ) & ( for n being Nat holds F1 . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom f holds
( F1 # x is convergent & lim (F1 # x) = f . x ) ) & ( for n being Nat holds K1 . n = integral' M,(F1 . n) ) & K1 is convergent & integral+ M,f = lim K1 ) by A1, Def15;

now

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 ;
( K1 . n = integral' M,(F1 . n) & F1 . n is_simple_func_in S & F1 . n is nonnegative ) by A2;
hence -infty < K1 . n1 by Th74; :: thesis: verum

end;

then A3: K1 is without-infty by Th16;
A4: for n, m being Nat st n <= m holds
K1 . n <= K1 . m

proof

let n, m be Nat; :: thesis: ( n <= m implies K1 . n <= K1 . m )
assume A5: n <= m ; :: thesis: K1 . n <= K1 . m
A6: ( K1 . n = integral' M,(F1 . n) & K1 . m = integral' M,(F1 . m) & F1 . n is_simple_func_in S & F1 . m is_simple_func_in S & dom (F1 . n) = dom f & dom (F1 . m) = dom f & F1 . n is nonnegative & F1 . m is nonnegative ) by A2;
A7: for x being set st x in dom ((F1 . m) - (F1 . n)) holds
(F1 . n) . x <= (F1 . m) . x

proof

let x be set ; :: 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 A2, A5, A6; :: thesis: verum

end;

then dom ((F1 . m) - (F1 . n)) = (dom (F1 . m)) /\ (dom (F1 . n)) by A6, Th75;
then ( (F1 . n) | (dom ((F1 . m) - (F1 . n))) = F1 . n & (F1 . m) | (dom ((F1 . m) - (F1 . n))) = F1 . m ) by A6, GRFUNC_1:64;
hence K1 . n <= K1 . m by A6, A7, Th76; :: thesis: verum

end;

consider A being Element of S such that
A8: ( A = dom f & f is_measurable_on A ) by A1;
A9: ( A = dom (c (#) f) & c (#) f is_measurable_on A ) by A8, MESFUNC1:41, MESFUNC1:def 6;
A10: c (#) f is nonnegative by A1, Th26;
deffunc H₁( Nat) -> Element of bool [:X,ExtREAL :] = c (#) (F1 . $1);
consider F being Functional_Sequence of X,ExtREAL such that
A11: for n being Nat holds F . n = H₁(n) from SEQFUNC:sch 1();
deffunc H₂( Nat) -> Element of ExtREAL = integral' M,(F . $1);
consider K being ExtREAL_sequence such that
A12: for n being Element of NAT holds K . n = H₂(n) from FUNCT_2:sch 4();

A13: now

let n be Nat; :: thesis: K . n = H₂(n)
n in NAT by ORDINAL1:def 13;
hence K . n = H₂(n) by A12; :: thesis: verum

end;

A14: for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom (c (#) f) )

proof

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 13;
A15: ( F1 . n is_simple_func_in S & F1 . n is nonnegative ) by A2;
A16: F . n1 = c (#) (F1 . n1) by A11;
hence F . n is_simple_func_in S by A15, Th45; :: thesis: dom (F . n) = dom (c (#) f)
thus dom (F . n) = dom (F1 . n) by A16, MESFUNC1:def 6
.= A by A2, A8
.= dom (c (#) f) by A8, MESFUNC1:def 6 ; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: F . n is nonnegative
reconsider n = n as Element of NAT by ORDINAL1:def 13;
F1 . n is nonnegative by A2;
then c (#) (F1 . n) is nonnegative by A1, Th26;
hence F . n is nonnegative by A11; :: thesis: verum

end;

A18: 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

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 A19: n <= m ; :: thesis: for x being Element of X st x in dom (c (#) f) holds
(F . n) . x <= (F . m) . x
let x be Element of X; :: thesis: ( x in dom (c (#) f) implies (F . n) . x <= (F . m) . x )
assume A20: x in dom (c (#) f) ; :: thesis: (F . n) . x <= (F . m) . x
reconsider n = n, m = m as Element of NAT by ORDINAL1:def 13;
( dom (c (#) (F1 . n)) = dom (F . n) & dom (c (#) (F1 . m)) = dom (F . m) ) by A11;
then A21: ( dom (c (#) (F1 . n)) = dom (c (#) f) & dom (c (#) (F1 . m)) = dom (c (#) f) ) by A14;
( (F . n) . x = (c (#) (F1 . n)) . x & (F . m) . x = (c (#) (F1 . m)) . x ) by A11;
then A22: ( (F . n) . x = (R_EAL c) * ((F1 . n) . x) & (F . m) . x = (R_EAL c) * ((F1 . m) . x) ) by A20, A21, MESFUNC1:def 6;
(F1 . n) . x <= (F1 . m) . x by A2, A8, A9, A19, A20;
hence (F . n) . x <= (F . m) . x by A1, A22, XXREAL_3:82; :: thesis: verum

end;

A23: 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 A24: x in dom (c (#) f) ; :: thesis: ( F # x is convergent & lim (F # x) = (c (#) f) . x )

A25: now

let n be Nat; :: thesis: (F # x) . n = (R_EAL c) * ((F1 # x) . n)
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
A26: dom (c (#) (F1 . n1)) = dom (F . n1) by A11
.= dom (c (#) f) by A14 ;
thus (F # x) . n = (F . n) . x by Def13
.= (c (#) (F1 . n1)) . x by A11
.= (R_EAL c) * ((F1 . n) . x) by A24, A26, MESFUNC1:def 6
.= (R_EAL c) * ((F1 # x) . n) by Def13 ; :: thesis: verum

end;

now

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 ;
B27: F1 . n is nonnegative by A2;
(F1 # x) . n = (F1 . n) . x by Def13;
hence -infty < (F1 # x) . n1 by B27, Def5; :: thesis: verum

end;

then A28: F1 # x is without-infty by Th16;

A29: now

let n, m be Nat; :: thesis: ( n <= m implies (F1 # x) . n <= (F1 # x) . m )
assume A30: n <= m ; :: thesis: (F1 # x) . n <= (F1 # x) . m
A31: (F1 # x) . n = (F1 . n) . x by Def13;
(F1 # x) . m = (F1 . m) . x by Def13;
hence (F1 # x) . n <= (F1 # x) . m by A2, A8, A9, A24, A30, A31; :: thesis: verum

end;

(R_EAL c) * (lim (F1 # x)) = (R_EAL c) * (f . x) by A2, A8, A9, A24
.= (c (#) f) . x by A24, MESFUNC1:def 6 ;
hence ( F # x is convergent & lim (F # x) = (c (#) f) . x ) by A1, A25, A28, A29, Th69; :: thesis: verum

end;

for n being Nat holds K . n = (R_EAL c) * (K1 . n)

proof

let n be Nat; :: thesis: K . n = (R_EAL c) * (K1 . n)
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
A32: ( F1 . n is_simple_func_in S & F1 . n is nonnegative ) by A2;
A33: F . n1 = c (#) (F1 . n1) by A11;
thus K . n = integral' M,(F . n1) by A13
.= (R_EAL c) * (integral' M,(F1 . n)) by A1, A32, A33, Th72
.= (R_EAL c) * (K1 . n) by A2 ; :: thesis: verum

end;

then ( K is convergent & lim K = (R_EAL c) * (lim K1) ) by A1, A3, A4, Th69;
hence integral+ M,(c (#) f) = (R_EAL c) * (integral+ M,f) by A2, A9, A10, A13, A14, A17, A18, A23, Def15; :: thesis: verum