let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let c be Real; :: thesis:
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:
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₁( 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₁(n) from SEQFUNC:sch 1();
A11: c (#) f is nonnegative by A1, A3, Th20;
A12: for n being Nat holds F . n is nonnegative

let n be Nat; :: thesis:
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:

end;

let n be Nat; :: thesis:
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:
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:

end;

let n, m be Nat; :: thesis:
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:
A27: for x being object st x in dom ((F1 . m) - (F1 . n)) holds
(F1 . n) . x <= (F1 . m) . x

let x be object ; :: thesis:
assume x in dom ((F1 . m) - (F1 . n)) ; :: thesis:
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:

end;

A28: F1 . n is_simple_func_in S by A4;
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:

end;

deffunc H₂( 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₂(n) from FUNCT_2:sch 4();

end;

let n be Nat; :: thesis:
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:

end;

let x be Element of X; :: thesis:

let n1 be set ; :: thesis:
assume n1 in dom (F1 # x) ; :: thesis:
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:

end;

let n be Nat; :: thesis:
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:

end;

let n, m be Nat; :: thesis:
assume A44: n <= m ; :: thesis:
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:

end;

c * (lim (F1 # x)) = c * (f . x) by A7, A13, A36, A40
.= (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:

end;

let n1 be set ; :: thesis:
assume n1 in dom K1 ; :: thesis:
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:

end;

then A47: K1 is () by Th10;
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

let n, m be Nat; :: thesis:
assume A50: n <= m ; :: thesis:
reconsider n = n, m = m as Element of NAT by ORDINAL1:def 12;
let x be Element of X; :: thesis:
assume A51: x in dom (c (#) f) ; :: thesis:
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:

end;