let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being object st x in F . n holds
f . x = a . n ) & ( for x being object st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) )
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being object st x in F . n holds
f . x = a . n ) & ( for x being object st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) )
let f be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being object st x in F . n holds
f . x = a . n ) & ( for x being object st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) ) )
assume f is_simple_func_in S ; :: thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being object st x in F . n holds
f . x = a . n ) & ( for x being object st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) )
then consider F being Finite_Sep_Sequence of S such that
A1: dom f = union (rng F) and
A2: for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y by MESFUNC2:def 4;
defpred S₁[ Nat, Element of ExtREAL ] means for x being set st x in F . $1 holds
$2 = f . x;
A3: for k being Nat st k in Seg (len F) holds
ex y being Element of ExtREAL st S₁[k,y]

proof

let k be Nat; :: thesis: ( k in Seg (len F) implies ex y being Element of ExtREAL st S₁[k,y] )
assume k in Seg (len F) ; :: thesis: ex y being Element of ExtREAL st S₁[k,y]
then A4: k in dom F by FINSEQ_1:def 3;
then A5: F . k in rng F by FUNCT_1:3;

per cases ( F . k = {} or F . k <> {} ) ;

suppose A6: F . k = {} ; :: thesis: ex y being Element of ExtREAL st S₁[k,y]

take y = 0. ; :: thesis: S₁[k,y]
for x being set st x in F . k holds
y = f . x by A6;
hence S₁[k,y] ; :: thesis: verum

end;

suppose F . k <> {} ; :: thesis: ex y being Element of ExtREAL st S₁[k,y]

then consider x1 being object such that
A7: x1 in F . k by XBOOLE_0:def 1;
reconsider x1 = x1 as set by TARSKI:1;
take y = f . x1; :: thesis: S₁[k,y]
for x being set st x in F . k holds
y = f . x

proof

let x be set ; :: thesis: ( x in F . k implies y = f . x )
A8: rng F c= bool X by XBOOLE_1:1;
then reconsider x1 = x1 as Element of X by A5, A7;
assume A9: x in F . k ; :: thesis: y = f . x
then reconsider x = x as Element of X by A5, A8;
f . x = f . x1 by A2, A4, A7, A9;
hence y = f . x ; :: thesis: verum

end;

hence S₁[k,y] ; :: thesis: verum

end;

end;

end;

consider a being FinSequence of ExtREAL such that
A10: ( dom a = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S₁[k,a . k] ) ) from FINSEQ_1:sch 5(A3);
take F ; :: thesis: ex a being FinSequence of ExtREAL st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being object st x in F . n holds
f . x = a . n ) & ( for x being object st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) )
take a ; :: thesis: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being object st x in F . n holds
f . x = a . n ) & ( for x being object st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) )
A11: for x being set st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) )

proof

let x be set ; :: thesis: ( x in dom f implies ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) )
assume x in dom f ; :: thesis: ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) )
deffunc H₁( Nat) -> Element of ExtREAL = (a . $1) * ((chi ((F . $1),X)) . x);
consider ax being FinSequence of ExtREAL such that
A12: ( len ax = len F & ( for k being Nat st k in dom ax holds
ax . k = H₁(k) ) ) from FINSEQ_2:sch 1();
take ax ; :: thesis: ( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) )
thus ( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) by A10, A12, FINSEQ_1:def 3; :: thesis: verum

end;

for n being Nat st n in dom F holds
for x being set st x in F . n holds
a . n = f . x

proof

let n be Nat; :: thesis: ( n in dom F implies for x being set st x in F . n holds
a . n = f . x )
assume n in dom F ; :: thesis: for x being set st x in F . n holds
a . n = f . x
then n in Seg (len F) by FINSEQ_1:def 3;
hence for x being set st x in F . n holds
a . n = f . x by A10; :: thesis: verum

end;

hence ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being object st x in F . n holds
f . x = a . n ) & ( for x being object st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) ) by A1, A10, A11, FINSEQ_1:def 3; :: thesis: verum