let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let f be non empty PartFunc of X,ExtREAL; :: thesis:
let M be sigma_Measure of S; :: thesis:
assume A1: f is_simple_func_in S ; :: thesis:
then consider E being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that
A2: E,b are_Re-presentation_of f by MESFUNC3:12;
A3: ( dom f = union (rng E) & dom E = dom b & ( for n being Nat st n in dom E holds
for x being object st x in E . n holds
f . x = b . n ) ) by A2, MESFUNC3:def 1;
reconsider E = E as non empty Finite_Sep_Sequence of S by A3, ZFMISC_1:2;
A4: for n being Nat st E . n <> {} holds
b . n in REAL

proof

let n be Nat; :: thesis:
assume A5: E . n <> {} ; :: thesis:
then consider x being object such that
A6: x in E . n by XBOOLE_0:def 1;
A7: n in dom E by A5, FUNCT_1:def 2;
then E . n in rng E by FUNCT_1:3;
then x in dom f by A3, A6, TARSKI:def 4;
then A8: f . x in rng f by FUNCT_1:3;
rng f is Subset of REAL by A1, MESFUNC2:def 4, MESFUNC2:32;
then f . x in REAL by A8;
hence b . n in REAL by A2, A6, A7, MESFUNC3:def 1; :: thesis:

end;

defpred S₁[ Nat, object ] means ( ( E . $1 <> {} implies $2 = b . $1 ) & ( E . $1 = {} implies $2 = 0 ) );
A9: for n being Nat st n in Seg (len E) holds
ex a being Element of ExtREAL st S₁[n,a]

proof

let n be Nat; :: thesis:
assume n in Seg (len E) ; :: thesis:

per cases ;

suppose A10: E . n <> {} ; :: thesis:

take a = b . n; :: thesis:
thus S₁[n,a] by A10; :: thesis:

end;

suppose A11: E . n = {} ; :: thesis:

take a = 0. ; :: thesis:
thus S₁[n,a] by A11; :: thesis:

end;

consider a being FinSequence of ExtREAL such that
A12: ( dom a = Seg (len E) & ( for n being Nat st n in Seg (len E) holds
S₁[n,a . n] ) ) from FINSEQ_1:sch 5(A9);
defpred S₂[ Nat, object ] means $2 = a . $1;
A13: for n being Nat st n in Seg (len E) holds
ex r being Element of REAL st S₂[n,r]

proof

let n be Nat; :: thesis:
assume A14: n in Seg (len E) ; :: thesis:

per cases ;

suppose A15: E . n <> {} ; :: thesis:

then a . n = b . n by A12, A14;
then reconsider r = a . n as Element of REAL by A4, A15;
take r ; :: thesis:
thus S₂[n,r] ; :: thesis:

end;

suppose E . n = {} ; :: thesis:

then a . n = 0 by A12, A14;
then reconsider r = a . n as Element of REAL by XREAL_0:def 1;
take r ; :: thesis:
thus S₂[n,r] ; :: thesis:

end;

consider r being FinSequence of REAL such that
A16: ( dom r = Seg (len E) & ( for n being Nat st n in Seg (len E) holds
S₂[n,r . n] ) ) from FINSEQ_1:sch 5(A13);
take E ; :: thesis:
take a ; :: thesis:
take r ; :: thesis:
A17: dom a = dom E by A12, FINSEQ_1:def 3;
A18: for n being Nat st n in dom E holds
for x being object st x in E . n holds
f . x = a . n

proof

let n be Nat; :: thesis:
assume A19: n in dom E ; :: thesis:
then A20: n in Seg (len E) by FINSEQ_1:def 3;
let x be object ; :: thesis:
assume A21: x in E . n ; :: thesis:
then f . x = b . n by A2, A19, MESFUNC3:def 1;
hence f . x = a . n by A12, A20, A21; :: thesis:

end;

hence E,a are_Re-presentation_of f by A3, A17, MESFUNC3:def 1; :: thesis:
thus for n being Nat holds
( a . n = r . n & f | (E . n) = (chi ((r . n),(E . n),X)) | (E . n) & ( E . n = {} implies r . n = 0 ) ) :: thesis:

proof

let n be Nat; :: thesis:

per cases ;

suppose A22: E . n <> {} ; :: thesis:

then A23: n in dom E by FUNCT_1:def 2;
then n in Seg (len E) by FINSEQ_1:def 3;
hence A24: a . n = r . n by A16; :: thesis:
E . n c= dom f by A3, A23, FUNCT_1:3, ZFMISC_1:74;
then A27: dom (f | (E . n)) = E . n by RELAT_1:62;
dom (chi ((r . n),(E . n),X)) = X by FUNCT_2:def 1;
then A28: dom ((chi ((r . n),(E . n),X)) | (E . n)) = dom (f | (E . n)) by A27, RELAT_1:62;
for x being Element of X st x in dom (f | (E . n)) holds
(f | (E . n)) . x = ((chi ((r . n),(E . n),X)) | (E . n)) . x

proof

let x be Element of X; :: thesis:
assume A29: x in dom (f | (E . n)) ; :: thesis:
then ((chi ((r . n),(E . n),X)) | (E . n)) . x = (chi ((r . n),(E . n),X)) . x by A27, FUNCT_1:49
.= a . n by A24, A27, A29, Def1
.= f . x by A18, A23, A27, A29 ;
hence (f | (E . n)) . x = ((chi ((r . n),(E . n),X)) | (E . n)) . x by A29, FUNCT_1:47; :: thesis:

end;

hence ( f | (E . n) = (chi ((r . n),(E . n),X)) | (E . n) & ( E . n = {} implies r . n = 0 ) ) by A22, A28, PARTFUN1:5; :: thesis:

end;

suppose z1: E . n = {} ; :: thesis:

now :: thesis:

per cases ;

suppose n in dom E ; :: thesis:

then A30: n in Seg (len E) by FINSEQ_1:def 3;
hence a . n = 0 by A12, z1; :: thesis:
hence r . n = 0 by A30, A16; :: thesis:

end;

suppose A31: not n in dom E ; :: thesis:

hence a . n = 0 by A17, FUNCT_1:def 2; :: thesis:
not n in Seg (len E) by A31, FINSEQ_1:def 3;
hence r . n = 0 by A16, FUNCT_1:def 2; :: thesis:

end;

hence ( a . n = r . n & f | (E . n) = (chi ((r . n),(E . n),X)) | (E . n) & ( E . n = {} implies r . n = 0 ) ) by z1; :: thesis:

end;