let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f, g be PartFunc of X,ExtREAL ; :: thesis:
let c be R_eal; :: thesis:
assume that
A1: f is_simple_func_in S and
A2: dom f <> {} and
A3: for x being set st x in dom f holds
0. <= f . x and
a4: ( 0. <= c & c < +infty ) and
A5: dom g = dom f and
A6: for x being set st x in dom g holds
g . x = c * (f . x) ; :: thesis:
( c <> -infty & c <> +infty ) by a4;
then A4: c in REAL by XXREAL_0:14;
consider F being Finite_Sep_Sequence of S, a, x being FinSequence of ExtREAL such that
A7: F,a are_Re-presentation_of f and
A8: dom x = dom F and
A9: for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) and
A10: integral X,S,M,f = Sum x by A1, A2, A3, Th4;
A11: f is real-valued by A1, MESFUNC2:def 5;
for x being Element of X st x in dom g holds
|.(g . x).| < +infty

proof

let x be Element of X; :: thesis:
assume A12: x in dom g ; :: thesis:
then |.(f . x).| < +infty by A5, A11, MESFUNC2:def 1;
then ( c * (f . x) <> +infty & c * (f . x) <> -infty ) by A4, EXTREAL2:67, XXREAL_3:80, XXREAL_3:81;
then ( g . x <> +infty & g . x <> -infty ) by A6, A12;
then ( -infty < g . x & g . x < +infty ) by XXREAL_0:4, XXREAL_0:6;
then ( - +infty < g . x & g . x < +infty ) by XXREAL_3:def 3;
hence |.(g . x).| < +infty by EXTREAL2:59; :: thesis:

end;

then A13: g is real-valued by MESFUNC2:def 1;
ex G being Finite_Sep_Sequence of S st
( dom g = union (rng G) & ( for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
g . x = g . y ) )

proof

consider G being Finite_Sep_Sequence of S such that
A14: dom f = union (rng G) and
A15: for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
f . x = f . y by A1, MESFUNC2:def 5;
A16: for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
g . x = g . y

proof

let n be Nat; :: thesis:
let x, y be Element of X; :: thesis:
assume A17: ( n in dom G & x in G . n & y in G . n ) ; :: thesis:
then G . n in rng G by FUNCT_1:12;
then ( x in dom g & y in dom g ) by A5, A14, A17, TARSKI:def 4;
then ( g . x = c * (f . x) & g . y = c * (f . y) ) by A6;
hence g . x = g . y by A15, A17; :: thesis:

end;

take G ; :: thesis:
thus ( dom g = union (rng G) & ( for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
g . x = g . y ) ) by A5, A14, A16; :: thesis:

end;

then A18: g is_simple_func_in S by A13, MESFUNC2:def 5;
A19: for x being set st x in dom g holds
0. <= g . x

proof

let x be set ; :: thesis:
assume A20: x in dom g ; :: thesis:
then 0. <= f . x by A3, A5;
then 0. <= c * (f . x) by a4;
hence 0. <= g . x by A6, A20; :: thesis:

end;

ex b being FinSequence of ExtREAL st
( dom b = dom a & ( for n being Nat st n in dom b holds
b . n = c * (a . n) ) )

proof

deffunc H₁( Nat) -> Element of ExtREAL = c * (a . $1);
consider b being FinSequence such that
A23: ( len b = len a & ( for n being Nat st n in dom b holds
b . n = H₁(n) ) ) from FINSEQ_1:sch 2();
A25: dom b = Seg (len b) by FINSEQ_1:def 3;
rng b c= ExtREAL

proof

let v be set ; :: according to TARSKI:def 3 :: thesis:
assume v in rng b ; :: thesis:
then consider k being set such that
A26: ( k in dom b & v = b . k ) by FUNCT_1:def 5;
reconsider k = k as Element of NAT by A26;
v = c * (a . k) by A23, A26;
hence v in ExtREAL ; :: thesis:

end;

then reconsider b = b as FinSequence of ExtREAL by FINSEQ_1:def 4;
take b ; :: thesis:
thus ( dom b = dom a & ( for n being Nat st n in dom b holds
b . n = c * (a . n) ) ) by A23, A25, FINSEQ_1:def 3; :: thesis:

end;

then consider b being FinSequence of ExtREAL such that
A27: dom b = dom a and
A28: for n being Nat st n in dom b holds
b . n = c * (a . n) ;
ex z being FinSequence of ExtREAL st
( dom z = dom x & ( for n being Nat st n in dom z holds
z . n = c * (x . n) ) )

proof

deffunc H₁( Nat) -> Element of ExtREAL = c * (x . $1);
consider z being FinSequence such that
A29: ( len z = len x & ( for n being Nat st n in dom z holds
z . n = H₁(n) ) ) from FINSEQ_1:sch 2();
A31: dom z = Seg (len z) by FINSEQ_1:def 3;
rng z c= ExtREAL

proof

let v be set ; :: according to TARSKI:def 3 :: thesis:
assume v in rng z ; :: thesis:
then consider k being set such that
A32: ( k in dom z & v = z . k ) by FUNCT_1:def 5;
reconsider k = k as Element of NAT by A32;
v = c * (x . k) by A29, A32;
hence v in ExtREAL ; :: thesis:

end;

then reconsider z = z as FinSequence of ExtREAL by FINSEQ_1:def 4;
take z ; :: thesis:
thus ( dom z = dom x & ( for n being Nat st n in dom z holds
z . n = c * (x . n) ) ) by A29, A31, FINSEQ_1:def 3; :: thesis:

end;

then consider z being FinSequence of ExtREAL such that
A33: dom z = dom x and
A34: for n being Nat st n in dom z holds
z . n = c * (x . n) ;
A35: F,b are_Re-presentation_of g

proof

A36: dom g = union (rng F) by A5, A7, MESFUNC3:def 1;
A37: dom F = dom b by A7, A27, MESFUNC3:def 1;

now

let n be Nat; :: thesis:
assume A38: n in dom F ; :: thesis:
let x be set ; :: thesis:
assume A39: x in F . n ; :: thesis:
F . n in rng F by A38, FUNCT_1:12;
then A40: x in dom g by A36, A39, TARSKI:def 4;
A41: n in dom b by A7, A27, A38, MESFUNC3:def 1;
thus g . x = c * (f . x) by A6, A40
.= c * (a . n) by A7, A38, A39, MESFUNC3:def 1
.= b . n by A28, A41 ; :: thesis:

end;

hence F,b are_Re-presentation_of g by A36, A37, MESFUNC3:def 1; :: thesis:

end;

for n being Nat st n in dom z holds
z . n = (b . n) * ((M * F) . n)

proof

let n be Nat; :: thesis:
assume A42: n in dom z ; :: thesis:
A43: dom a = dom F by A7, MESFUNC3:def 1;
thus z . n = c * (x . n) by A34, A42
.= c * ((a . n) * ((M * F) . n)) by A9, A33, A42
.= (c * (a . n)) * ((M * F) . n) by XXREAL_3:77
.= (b . n) * ((M * F) . n) by A8, A27, A28, A33, A42, A43 ; :: thesis:

end;

hence integral X,S,M,g = Sum z by A2, A5, A8, A18, A19, A33, A35, Th3
.= c * (integral X,S,M,f) by A4, A10, A33, A34, MESFUNC3:10 ;
:: thesis: