let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being R_eal st 0 <= c & f is_simple_func_in S & ( for x being object st x in dom f holds

f . x = c ) holds

integral' (M,f) = c * (M . (dom f))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being R_eal st 0 <= c & f is_simple_func_in S & ( for x being object st x in dom f holds

f . x = c ) holds

integral' (M,f) = c * (M . (dom f))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for c being R_eal st 0 <= c & f is_simple_func_in S & ( for x being object st x in dom f holds

f . x = c ) holds

integral' (M,f) = c * (M . (dom f))

let f be PartFunc of X,ExtREAL; :: thesis: for c being R_eal st 0 <= c & f is_simple_func_in S & ( for x being object st x in dom f holds

f . x = c ) holds

integral' (M,f) = c * (M . (dom f))

let c be R_eal; :: thesis: ( 0 <= c & f is_simple_func_in S & ( for x being object st x in dom f holds

f . x = c ) implies integral' (M,f) = c * (M . (dom f)) )

assume that

A1: 0 <= c and

A2: f is_simple_func_in S and

A3: for x being object st x in dom f holds

f . x = c ; :: thesis: integral' (M,f) = c * (M . (dom f))

for x being object st x in dom f holds

0 <= f . x by A1, A3;

then a4: f is nonnegative by SUPINF_2:52;

reconsider A = dom f as Element of S by A2, Th37;

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being R_eal st 0 <= c & f is_simple_func_in S & ( for x being object st x in dom f holds

f . x = c ) holds

integral' (M,f) = c * (M . (dom f))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for c being R_eal st 0 <= c & f is_simple_func_in S & ( for x being object st x in dom f holds

f . x = c ) holds

integral' (M,f) = c * (M . (dom f))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for c being R_eal st 0 <= c & f is_simple_func_in S & ( for x being object st x in dom f holds

f . x = c ) holds

integral' (M,f) = c * (M . (dom f))

let f be PartFunc of X,ExtREAL; :: thesis: for c being R_eal st 0 <= c & f is_simple_func_in S & ( for x being object st x in dom f holds

f . x = c ) holds

integral' (M,f) = c * (M . (dom f))

let c be R_eal; :: thesis: ( 0 <= c & f is_simple_func_in S & ( for x being object st x in dom f holds

f . x = c ) implies integral' (M,f) = c * (M . (dom f)) )

assume that

A1: 0 <= c and

A2: f is_simple_func_in S and

A3: for x being object st x in dom f holds

f . x = c ; :: thesis: integral' (M,f) = c * (M . (dom f))

for x being object st x in dom f holds

0 <= f . x by A1, A3;

then a4: f is nonnegative by SUPINF_2:52;

reconsider A = dom f as Element of S by A2, Th37;

per cases
( dom f = {} or dom f <> {} )
;

end;

suppose A5:
dom f = {}
; :: thesis: integral' (M,f) = c * (M . (dom f))

then A6:
M . A = 0
by VALUED_0:def 19;

integral' (M,f) = 0 by A5, Def14;

hence integral' (M,f) = c * (M . (dom f)) by A6; :: thesis: verum

end;integral' (M,f) = 0 by A5, Def14;

hence integral' (M,f) = c * (M . (dom f)) by A6; :: thesis: verum

suppose A7:
dom f <> {}
; :: thesis: integral' (M,f) = c * (M . (dom f))

set x = <*(c * (M . A))*>;

reconsider a = <*c*> as FinSequence of ExtREAL ;

set F = <*(dom f)*>;

reconsider x = <*(c * (M . A))*> as FinSequence of ExtREAL ;

A8: rng <*(dom f)*> = {A} by FINSEQ_1:38;

rng <*(dom f)*> c= S

for i, j being Nat st i in dom F & j in dom F & i <> j holds

F . i misses F . j

A13: dom F = Seg 1 by FINSEQ_1:38

.= dom a by FINSEQ_1:38 ;

A14: for n being Nat st n in dom F holds

for x being object st x in F . n holds

f . x = a . n

x . n = c * (M . A)

.= dom F by FINSEQ_1:38 ;

A18: for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n)

then F,a are_Re-presentation_of f by A13, A14, MESFUNC3:def 1;

then integral (M,f) = Sum x by A2, a4, A7, A17, A18, MESFUNC4:3;

then A22: integral' (M,f) = Sum x by A7, Def14;

reconsider j = 1 as R_eal by XXREAL_0:def 1;

1 = len x by FINSEQ_1:40;

then Sum x = j * (c * (M . A)) by A16, MESFUNC3:18;

hence integral' (M,f) = c * (M . (dom f)) by A22, XXREAL_3:81; :: thesis: verum

end;reconsider a = <*c*> as FinSequence of ExtREAL ;

set F = <*(dom f)*>;

reconsider x = <*(c * (M . A))*> as FinSequence of ExtREAL ;

A8: rng <*(dom f)*> = {A} by FINSEQ_1:38;

rng <*(dom f)*> c= S

proof

then reconsider F = <*(dom f)*> as FinSequence of S by FINSEQ_1:def 4;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng <*(dom f)*> or z in S )

assume z in rng <*(dom f)*> ; :: thesis: z in S

then z = A by A8, TARSKI:def 1;

hence z in S ; :: thesis: verum

end;assume z in rng <*(dom f)*> ; :: thesis: z in S

then z = A by A8, TARSKI:def 1;

hence z in S ; :: thesis: verum

for i, j being Nat st i in dom F & j in dom F & i <> j holds

F . i misses F . j

proof

then reconsider F = F as Finite_Sep_Sequence of S by MESFUNC3:4;
let i, j be Nat; :: thesis: ( i in dom F & j in dom F & i <> j implies F . i misses F . j )

assume that

A9: i in dom F and

A10: j in dom F and

A11: i <> j ; :: thesis: F . i misses F . j

A12: dom F = {1} by FINSEQ_1:2, FINSEQ_1:38;

then i = 1 by A9, TARSKI:def 1;

hence F . i misses F . j by A10, A11, A12, TARSKI:def 1; :: thesis: verum

end;assume that

A9: i in dom F and

A10: j in dom F and

A11: i <> j ; :: thesis: F . i misses F . j

A12: dom F = {1} by FINSEQ_1:2, FINSEQ_1:38;

then i = 1 by A9, TARSKI:def 1;

hence F . i misses F . j by A10, A11, A12, TARSKI:def 1; :: thesis: verum

A13: dom F = Seg 1 by FINSEQ_1:38

.= dom a by FINSEQ_1:38 ;

A14: for n being Nat st n in dom F holds

for x being object st x in F . n holds

f . x = a . n

proof

A16:
for n being Nat st n in dom x holds
let n be Nat; :: thesis: ( n in dom F implies for x being object st x in F . n holds

f . x = a . n )

assume n in dom F ; :: thesis: for x being object st x in F . n holds

f . x = a . n

then n in {1} by FINSEQ_1:2, FINSEQ_1:38;

then A15: n = 1 by TARSKI:def 1;

let x be object ; :: thesis: ( x in F . n implies f . x = a . n )

assume x in F . n ; :: thesis: f . x = a . n

then x in dom f by A15, FINSEQ_1:40;

then f . x = c by A3;

hence f . x = a . n by A15, FINSEQ_1:40; :: thesis: verum

end;f . x = a . n )

assume n in dom F ; :: thesis: for x being object st x in F . n holds

f . x = a . n

then n in {1} by FINSEQ_1:2, FINSEQ_1:38;

then A15: n = 1 by TARSKI:def 1;

let x be object ; :: thesis: ( x in F . n implies f . x = a . n )

assume x in F . n ; :: thesis: f . x = a . n

then x in dom f by A15, FINSEQ_1:40;

then f . x = c by A3;

hence f . x = a . n by A15, FINSEQ_1:40; :: thesis: verum

x . n = c * (M . A)

proof

A17: dom x =
Seg 1
by FINSEQ_1:38
let n be Nat; :: thesis: ( n in dom x implies x . n = c * (M . A) )

assume n in dom x ; :: thesis: x . n = c * (M . A)

then n in {1} by FINSEQ_1:2, FINSEQ_1:38;

then n = 1 by TARSKI:def 1;

hence x . n = c * (M . A) by FINSEQ_1:40; :: thesis: verum

end;assume n in dom x ; :: thesis: x . n = c * (M . A)

then n in {1} by FINSEQ_1:2, FINSEQ_1:38;

then n = 1 by TARSKI:def 1;

hence x . n = c * (M . A) by FINSEQ_1:40; :: thesis: verum

.= dom F by FINSEQ_1:38 ;

A18: for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n)

proof

dom f = union (rng F)
by A8, ZFMISC_1:25;
let n be Nat; :: thesis: ( n in dom x implies x . n = (a . n) * ((M * F) . n) )

assume A19: n in dom x ; :: thesis: x . n = (a . n) * ((M * F) . n)

then n in {1} by FINSEQ_1:2, FINSEQ_1:38;

then A20: n = 1 by TARSKI:def 1;

then A21: x . n = c * (M . A) by FINSEQ_1:40;

(M * F) . n = M . (F . n) by A17, A19, FUNCT_1:13

.= M . A by A20, FINSEQ_1:40 ;

hence x . n = (a . n) * ((M * F) . n) by A20, A21, FINSEQ_1:40; :: thesis: verum

end;assume A19: n in dom x ; :: thesis: x . n = (a . n) * ((M * F) . n)

then n in {1} by FINSEQ_1:2, FINSEQ_1:38;

then A20: n = 1 by TARSKI:def 1;

then A21: x . n = c * (M . A) by FINSEQ_1:40;

(M * F) . n = M . (F . n) by A17, A19, FUNCT_1:13

.= M . A by A20, FINSEQ_1:40 ;

hence x . n = (a . n) * ((M * F) . n) by A20, A21, FINSEQ_1:40; :: thesis: verum

then F,a are_Re-presentation_of f by A13, A14, MESFUNC3:def 1;

then integral (M,f) = Sum x by A2, a4, A7, A17, A18, MESFUNC4:3;

then A22: integral' (M,f) = Sum x by A7, Def14;

reconsider j = 1 as R_eal by XXREAL_0:def 1;

1 = len x by FINSEQ_1:40;

then Sum x = j * (c * (M . A)) by A16, MESFUNC3:18;

hence integral' (M,f) = c * (M . (dom f)) by A22, XXREAL_3:81; :: thesis: verum