let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let c be R_eal; :: thesis:
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:
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;

suppose A5: dom f = {} ; :: thesis:

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:

end;

suppose A7: dom f <> {} ; :: thesis:

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

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng <*(dom f)*> ; :: thesis:
then z = A by A8, TARSKI:def 1;
hence z in S ; :: thesis:

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

let i, j be Nat; :: thesis:
assume that
A9: i in dom F and
A10: j in dom F and
A11: i <> j ; :: thesis:
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:

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

let n be Nat; :: thesis:
assume n in dom F ; :: thesis:
then n in {1} by FINSEQ_1:2, FINSEQ_1:38;
then A15: n = 1 by TARSKI:def 1;
let x be object ; :: thesis:
assume x in F . n ; :: thesis:
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:

end;

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

let n be Nat; :: thesis:
assume n in dom x ; :: thesis:
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:

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)

let n be Nat; :: thesis:
assume A19: n in dom x ; :: thesis:
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:

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:

end;

end;