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 set 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 set 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 set 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 set 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 set 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 set st x in dom f holds
f . x = c ; :: thesis: integral' M,f = c * (M . (dom f))
reconsider A = dom f as Element of S by A2, Th43;
A4: for x being set st x in dom f holds
0 <= f . x by A1, A3;

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

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

then A6: integral' M,f = 0 by Def14;
M . A = 0 by A5, VALUED_0:def 19;
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 F = <*(dom f)*>;
A8: rng <*(dom f)*> = {A} by FINSEQ_1:55;
rng <*(dom f)*> c= S

proof

let z be set ; :: 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 A9: ( i in dom F & j in dom F & i <> j ) ; :: thesis: F . i misses F . j
dom F = {1} by FINSEQ_1:4, FINSEQ_1:55;
then ( i = 1 & j = 1 ) by A9, TARSKI:def 1;
hence F . i misses F . j by A9; :: thesis: verum

end;

then reconsider F = F as Finite_Sep_Sequence of S by MESFUNC3:4;
reconsider a = <*c*> as FinSequence of ExtREAL ;
A10: dom f = union (rng F) by A8, ZFMISC_1:31;
A11: dom F = Seg 1 by FINSEQ_1:55
.= dom a by FINSEQ_1:55 ;
for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n

proof

let n be Nat; :: thesis: ( n in dom F implies for x being set st x in F . n holds
f . x = a . n )
assume A12: n in dom F ; :: thesis: for x being set st x in F . n holds
f . x = a . n
let x be set ; :: thesis: ( x in F . n implies f . x = a . n )
assume A13: x in F . n ; :: thesis: f . x = a . n
n in {1} by A12, FINSEQ_1:4, FINSEQ_1:55;
then A14: n = 1 by TARSKI:def 1;
then x in dom f by A13, FINSEQ_1:57;
then f . x = c by A3;
hence f . x = a . n by A14, FINSEQ_1:57; :: thesis: verum

end;

then A15: F,a are_Re-presentation_of f by A10, A11, MESFUNC3:def 1;
set x = <*(c * (M . A))*>;
reconsider x = <*(c * (M . A))*> as FinSequence of ExtREAL ;
A16: dom x = Seg 1 by FINSEQ_1:55
.= dom F by FINSEQ_1:55 ;
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 A17: n in dom x ; :: thesis: x . n = (a . n) * ((M * F) . n)
then n in {1} by FINSEQ_1:4, FINSEQ_1:55;
then A18: n = 1 by TARSKI:def 1;
then A19: x . n = c * (M . A) by FINSEQ_1:57;
(M * F) . n = M . (F . n) by A16, A17, FUNCT_1:23
.= M . A by A18, FINSEQ_1:57 ;
hence x . n = (a . n) * ((M * F) . n) by A18, A19, FINSEQ_1:57; :: thesis: verum

end;

then integral X,S,M,f = Sum x by A2, A4, A7, A15, A16, MESFUNC4:3;
then A20: integral' M,f = Sum x by A7, Def14;
A21: 1 = len x by FINSEQ_1:57;
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:4, FINSEQ_1:55;
then n = 1 by TARSKI:def 1;
hence x . n = c * (M . A) by FINSEQ_1:57; :: thesis: verum

end;

then Sum x = (R_EAL 1) * (c * (M . A)) by A21, MESFUNC3:18;
hence integral' M,f = c * (M . (dom f)) by A20, XXREAL_3:92; :: thesis: verum

end;

end;