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 ;
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 ;
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 ;
then y in dom g by ;
then A17: g . y = c * (f . y) by A7;
x in dom g by ;
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 ; :: 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 H1( 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 = H1(n) ) ) from 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:
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 ;
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 ;
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 ; :: 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 ;
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 H1( 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 = H1(n) ) ) from 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:
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 ;
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 ;
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 ; :: 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 ;
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
.= (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 ;
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 ;
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 ;
then x in dom g by ;
hence g . x = c * (f . x) by A7
.= c * (a . n) by
.= b . n by ;
:: thesis: verum
end;
dom F = dom b by ;
then A45: F,b are_Re-presentation_of g by ;
A46: f is V70() by ;
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 ;
then g . x <> -infty by ;
then -infty < g . x by XXREAL_0:6;
then A48: - +infty < g . x by XXREAL_3:def 3;
c * (f . x) <> +infty by ;
then g . x <> +infty by ;
then g . x < +infty by XXREAL_0:4;
hence |.(g . x).| < +infty by ; :: thesis: verum
end;
then g is V70() by MESFUNC2:def 1;
then g is_simple_func_in S by ;
hence integral (M,g) = Sum z by A2, A6, A19, A35, A45, A37, Th3, X
.= c * (integral (M,f)) by ;
:: thesis: verum