let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL
for c being R_eal st f is_simple_func_in S & dom f <> {} & f is nonnegative & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds
g . x = c * (f . x) ) holds
integral (M,g) = c * (integral (M,f))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL
for c being R_eal st f is_simple_func_in S & dom f <> {} & f is nonnegative & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds
g . x = c * (f . x) ) holds
integral (M,g) = c * (integral (M,f))
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL
for c being R_eal st f is_simple_func_in S & dom f <> {} & f is nonnegative & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds
g . x = c * (f . x) ) holds
integral (M,g) = c * (integral (M,f))
let f, g be PartFunc of X,ExtREAL; :: thesis: for c being R_eal st f is_simple_func_in S & dom f <> {} & f is nonnegative & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds
g . x = c * (f . x) ) holds
integral (M,g) = c * (integral (M,f))
let c be R_eal; :: thesis: ( f is_simple_func_in S & dom f <> {} & f is nonnegative & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds
g . x = c * (f . x) ) implies integral (M,g) = c * (integral (M,f)) )
assume that
A1: f is_simple_func_in S and
A2: dom f <> {} and
A3: f is nonnegative and
A4: 0. <= c and
A5: c < +infty and
A6: dom g = dom f and
A7: for x being set st x in dom g holds
g . x = c * (f . x) ; :: thesis: integral (M,g) = c * (integral (M,f))
for x being object st x in dom g holds
0. <= g . x

proof

let x be object ; :: thesis: ( x in dom g implies 0. <= g . x )
assume A9: x in dom g ; :: thesis: 0. <= g . x
0. <= f . x by A3, SUPINF_2:51;
then 0. <= c * (f . x) by A4;
hence 0. <= g . x by A7, A9; :: thesis: verum

end;

then X: g is nonnegative by SUPINF_2:52;
A10: 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
A11: dom f = union (rng G) and
A12: 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 4;
take G ; :: thesis: ( 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 ) )
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: 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
let x, y be Element of X; :: thesis: ( n in dom G & x in G . n & y in G . n implies g . x = g . y )
assume that
A13: n in dom G and
A14: x in G . n and
A15: y in G . n ; :: thesis: g . x = g . y
A16: G . n in rng G by A13, FUNCT_1:3;
then y in dom g by A6, A11, A15, TARSKI:def 4;
then A17: g . y = c * (f . y) by A7;
x in dom g by A6, A11, A14, A16, TARSKI:def 4;
then g . x = c * (f . x) by A7;
hence g . x = g . y by A12, A13, A14, A15, A17; :: thesis: verum

end;

hence ( 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 A6, A11; :: thesis: verum

end;

consider F being Finite_Sep_Sequence of S, a, x being FinSequence of ExtREAL such that
A18: F,a are_Re-presentation_of f and
A19: dom x = dom F and
A20: for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) and
A21: integral (M,f) = Sum x by A1, A2, A3, Th4;
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
A22: ( len b = len a & ( for n being Nat st n in dom b holds
b . n = H₁(n) ) ) from FINSEQ_1:sch 2();
A23: rng b c= ExtREAL

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in rng b or v in ExtREAL )
assume v in rng b ; :: thesis: v in ExtREAL
then consider k being object such that
A24: k in dom b and
A25: v = b . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A24;
v = c * (a . k) by A22, A24, A25;
hence v in ExtREAL ; :: thesis: verum

end;

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

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) ;
A29: c in REAL by A4, A5, XXREAL_0:14;
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
A30: ( len z = len x & ( for n being Nat st n in dom z holds
z . n = H₁(n) ) ) from FINSEQ_1:sch 2();
A31: rng z c= ExtREAL

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in rng z or v in ExtREAL )
assume v in rng z ; :: thesis: v in ExtREAL
then consider k being object such that
A32: k in dom z and
A33: v = z . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A32;
v = c * (x . k) by A30, A32, A33;
hence v in ExtREAL ; :: thesis: verum

end;

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

end;

then consider z being FinSequence of ExtREAL such that
A35: dom z = dom x and
A36: for n being Nat st n in dom z holds
z . n = c * (x . n) ;
A37: for n being Nat st n in dom z holds
z . n = (b . n) * ((M * F) . n)

proof

let n be Nat; :: thesis: ( n in dom z implies z . n = (b . n) * ((M * F) . n) )
A38: dom a = dom F by A18, MESFUNC3:def 1;
assume A39: n in dom z ; :: thesis: z . n = (b . n) * ((M * F) . n)
hence z . n = c * (x . n) by A36
.= c * ((a . n) * ((M * F) . n)) by A20, A35, A39
.= (c * (a . n)) * ((M * F) . n) by XXREAL_3:66
.= (b . n) * ((M * F) . n) by A19, A27, A28, A35, A39, A38 ;
:: thesis: verum

end;

A40: dom g = union (rng F) by A6, A18, MESFUNC3:def 1;

A41: now :: thesis: for n being Nat st n in dom F holds
for x being object st x in F . n holds
g . x = b . n

let n be Nat; :: thesis: ( n in dom F implies for x being object st x in F . n holds
g . x = b . n )
assume A42: n in dom F ; :: thesis: for x being object st x in F . n holds
g . x = b . n
then A43: n in dom b by A18, A27, MESFUNC3:def 1;
let x be object ; :: thesis: ( x in F . n implies g . x = b . n )
assume A44: x in F . n ; :: thesis: g . x = b . n
F . n in rng F by A42, FUNCT_1:3;
then x in dom g by A40, A44, TARSKI:def 4;
hence g . x = c * (f . x) by A7
.= c * (a . n) by A18, A42, A44, MESFUNC3:def 1
.= b . n by A28, A43 ;
:: thesis: verum

end;

dom F = dom b by A18, A27, MESFUNC3:def 1;
then A45: F,b are_Re-presentation_of g by A40, A41, MESFUNC3:def 1;
A46: f is real-valued by A1, MESFUNC2:def 4;
for x being Element of X st x in dom g holds
|.(g . x).| < +infty

proof

let x be Element of X; :: thesis: ( x in dom g implies |.(g . x).| < +infty )
assume A47: x in dom g ; :: thesis: |.(g . x).| < +infty
c * (f . x) <> -infty by A29, A46;
then g . x <> -infty by A7, A47;
then -infty < g . x by XXREAL_0:6;
then A48: - +infty < g . x by XXREAL_3:def 3;
c * (f . x) <> +infty by A29, A46;
then g . x <> +infty by A7, A47;
then g . x < +infty by XXREAL_0:4;
hence |.(g . x).| < +infty by A48, EXTREAL1:22; :: thesis: verum

end;

then g is real-valued by MESFUNC2:def 1;
then g is_simple_func_in S by A10, MESFUNC2:def 4;
hence integral (M,g) = Sum z by A2, A6, A19, A35, A45, A37, Th3, X
.= c * (integral (M,f)) by A29, A21, A35, A36, MESFUNC3:10 ;
:: thesis: verum