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

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 ) )

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) ) )

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) ) )

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)

then A45: F,b are_Re-presentation_of g by A40, A41, MESFUNC3:def 1;

A46: f is V70() by A1, MESFUNC2:def 4;

for x being Element of X st x in dom g holds

|.(g . x).| < +infty

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

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

then X:
g is nonnegative
by SUPINF_2:52;
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;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

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 F being Finite_Sep_Sequence of S, a, x being FinSequence of ExtREAL such that
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

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;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

hence
( dom g = union (rng G) & ( for n being Nat
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;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

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

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

then consider b being FinSequence of ExtREAL such that
deffunc H_{1}( 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_{1}(n) ) )
from FINSEQ_1:sch 2();

A23: rng b c= ExtREAL

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;consider b being FinSequence such that

A22: ( len b = len a & ( for n being Nat st n in dom b holds

b . n = H

A23: rng b c= ExtREAL

proof

A26:
dom b = Seg (len b)
by FINSEQ_1:def 3;
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;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

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

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

then consider z being FinSequence of ExtREAL such that
deffunc H_{1}( 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_{1}(n) ) )
from FINSEQ_1:sch 2();

A31: rng z c= ExtREAL

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;consider z being FinSequence such that

A30: ( len z = len x & ( for n being Nat st n in dom z holds

z . n = H

A31: rng z c= ExtREAL

proof

A34:
dom z = Seg (len z)
by FINSEQ_1:def 3;
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;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

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

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

A40:
dom g = union (rng F)
by A6, A18, MESFUNC3:def 1;
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;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

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

dom F = dom b
by A18, A27, MESFUNC3:def 1;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;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

then A45: F,b are_Re-presentation_of g by A40, A41, MESFUNC3:def 1;

A46: f is V70() by A1, MESFUNC2:def 4;

for x being Element of X st x in dom g holds

|.(g . x).| < +infty

proof

then
g is V70()
by MESFUNC2:def 1;
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;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

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