let X be non empty set ; :: thesis: for S being SigmaField of X
for f being non empty PartFunc of X,ExtREAL
for M being sigma_Measure of S st f is_simple_func_in S holds
ex E being non empty Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL ex r being FinSequence of REAL st
( E,a are_Re-presentation_of f & ( 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 ) ) ) )
let S be SigmaField of X; :: thesis: for f being non empty PartFunc of X,ExtREAL
for M being sigma_Measure of S st f is_simple_func_in S holds
ex E being non empty Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL ex r being FinSequence of REAL st
( E,a are_Re-presentation_of f & ( 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 ) ) ) )
let f be non empty PartFunc of X,ExtREAL; :: thesis: for M being sigma_Measure of S st f is_simple_func_in S holds
ex E being non empty Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL ex r being FinSequence of REAL st
( E,a are_Re-presentation_of f & ( 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 ) ) ) )
let M be sigma_Measure of S; :: thesis: ( f is_simple_func_in S implies ex E being non empty Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL ex r being FinSequence of REAL st
( E,a are_Re-presentation_of f & ( 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 ) ) ) ) )
assume A1: f is_simple_func_in S ; :: thesis: ex E being non empty Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL ex r being FinSequence of REAL st
( E,a are_Re-presentation_of f & ( 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 ) ) ) )
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: ( E . n <> {} implies b . n in REAL )
assume A5: E . n <> {} ; :: thesis: b . n in REAL
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: verum
end;
defpred S1[ 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 S1[n,a]
proof
let n be Nat; :: thesis: ( n in Seg (len E) implies ex a being Element of ExtREAL st S1[n,a] )
assume n in Seg (len E) ; :: thesis: ex a being Element of ExtREAL st S1[n,a]
per cases ( E . n <> {} or E . n = {} ) ;
suppose A10: E . n <> {} ; :: thesis: ex a being Element of ExtREAL st S1[n,a]
take a = b . n; :: thesis: S1[n,a]
thus S1[n,a] by A10; :: thesis: verum
end;
suppose A11: E . n = {} ; :: thesis: ex a being Element of ExtREAL st S1[n,a]
take a = 0. ; :: thesis: S1[n,a]
thus S1[n,a] by A11; :: thesis: verum
end;
end;
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
S1[n,a . n] ) ) from FINSEQ_1:sch 5(A9);
 defpred S2[ 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 S2[n,r]
proof
let n be Nat; :: thesis: ( n in Seg (len E) implies ex r being Element of REAL st S2[n,r] )
assume A14: n in Seg (len E) ; :: thesis: ex r being Element of REAL st S2[n,r]
per cases ( E . n <> {} or E . n = {} ) ;
suppose A15: E . n <> {} ; :: thesis: ex r being Element of REAL st S2[n,r]
then a . n = b . n by A12, A14;
then reconsider r = a . n as Element of REAL by A4, A15;
take r ; :: thesis: S2[n,r]
thus S2[n,r] ; :: thesis: verum
end;
suppose E . n = {} ; :: thesis: ex r being Element of REAL st S2[n,r]
then a . n = 0 by A12, A14;
then reconsider r = a . n as Element of REAL by XREAL_0:def 1;
take r ; :: thesis: S2[n,r]
thus S2[n,r] ; :: thesis: verum
end;
end;
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
S2[n,r . n] ) ) from FINSEQ_1:sch 5(A13);
 take E ; :: thesis: ex a being FinSequence of ExtREAL ex r being FinSequence of REAL st
( E,a are_Re-presentation_of f & ( 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 ) ) ) )
take a ; :: thesis: ex r being FinSequence of REAL st
( E,a are_Re-presentation_of f & ( 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 ) ) ) )
take r ; :: thesis: ( E,a are_Re-presentation_of f & ( 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 ) ) ) )
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: ( n in dom E implies for x being object st x in E . n holds
f . x = a . n )
assume A19: n in dom E ; :: thesis: for x being object st x in E . n holds
f . x = a . n
then A20: n in Seg (len E) by FINSEQ_1:def 3;
let x be object ; :: thesis: ( x in E . n implies f . x = a . n )
assume A21: x in E . n ; :: thesis: f . x = a . n
then f . x = b . n by A2, A19, MESFUNC3:def 1;
hence f . x = a . n by A12, A20, A21; :: thesis: verum
end;
hence E,a are_Re-presentation_of f by A3, A17, MESFUNC3:def 1; :: thesis: 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 ) )
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: verum
proof
let n be Nat; :: thesis: ( a . n = r . n & f | (E . n) = (chi ((r . n),(E . n),X)) | (E . n) & ( E . n = {} implies r . n = 0 ) )
per cases ( E . n <> {} or E . n = {} ) ;
suppose A22: E . n <> {} ; :: thesis: ( a . n = r . n & f | (E . n) = (chi ((r . n),(E . n),X)) | (E . n) & ( E . n = {} implies r . n = 0 ) )
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: ( f | (E . n) = (chi ((r . n),(E . n),X)) | (E . n) & ( E . n = {} implies r . n = 0 ) )
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: ( x in dom (f | (E . n)) implies (f | (E . n)) . x = ((chi ((r . n),(E . n),X)) | (E . n)) . x )
assume A29: x in dom (f | (E . n)) ; :: thesis: (f | (E . n)) . x = ((chi ((r . n),(E . n),X)) | (E . n)) . x
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: verum
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: verum
end;
suppose z1: E . n = {} ; :: thesis: ( a . n = r . n & f | (E . n) = (chi ((r . n),(E . n),X)) | (E . n) & ( E . n = {} implies r . n = 0 ) )
now :: thesis: ( a . n = 0 & r . n = 0 )
per cases ( n in dom E or not n in dom E ) ;
suppose n in dom E ; :: thesis: ( a . n = 0 & r . n = 0 )
then A30: n in Seg (len E) by FINSEQ_1:def 3;
hence a . n = 0 by A12, z1; :: thesis: r . n = 0
hence r . n = 0 by A30, A16; :: thesis: verum
end;
end;
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: verum
end;
end;
end;