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;

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

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;

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

proof

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;

then reconsider F = <*(dom f)*> as FinSequence of S by FINSEQ_1:def 4;
for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j

proof

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;

then reconsider F = F as Finite_Sep_Sequence of S by MESFUNC3:4;
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

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;
then f . x = c by A3;
hence f . x = a . n by A15; :: thesis: verum

end;

A16: for n being Nat st n in dom x holds
x . n = c * (M . A)

proof

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) ; :: thesis: verum

end;

A17: dom x = Seg 1 by FINSEQ_1:38
.= 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

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;
(M * F) . n = M . (F . n) by A17, A19, FUNCT_1:13
.= M . A by A20 ;
hence x . n = (a . n) * ((M * F) . n) by A20; :: thesis: verum

end;

dom f = union (rng F) by A8, ZFMISC_1:25;
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;

end;