let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) )

let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) )

let f be PartFunc of X,COMPLEX; :: thesis: ( f is_simple_func_in S implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) ) )

assume f is_simple_func_in S ; :: thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) )

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 ;
defpred S1[ set , set ] 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 COMPLEX st S1[k,y]
proof
let k be Nat; :: thesis: ( k in Seg (len F) implies ex y being Element of COMPLEX st S1[k,y] )
assume k in Seg (len F) ; :: thesis: ex y being Element of COMPLEX st S1[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 COMPLEX st S1[k,y]
0 in REAL by XREAL_0:def 1;
then reconsider y = 0 as Element of COMPLEX by NUMBERS:11;
take y ; :: thesis: S1[k,y]
thus S1[k,y] by A6; :: thesis: verum
end;
suppose F . k <> {} ; :: thesis: ex y being Element of COMPLEX st S1[k,y]
then consider x1 being object such that
A7: x1 in F . k by XBOOLE_0:def 1;
x1 in dom f by ;
then f . x1 in rng f by FUNCT_1:3;
then reconsider y = f . x1 as Element of COMPLEX ;
take y ; :: thesis: S1[k,y]
hereby :: thesis: verum
let x be set ; :: thesis: ( x in F . k implies y = f . x )
A8: rng F c= bool X by XBOOLE_1:1;
assume x in F . k ; :: thesis: y = f . x
hence y = f . x by A2, A4, A5, A7, A8; :: thesis: verum
end;
end;
end;
end;
consider a being FinSequence of COMPLEX such that
A9: ( dom a = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S1[k,a . k] ) ) from take F ; :: thesis: ex a being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) )

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 set st x in F . n holds
f . x = a . n ) )

now :: thesis: for n being Nat st n in dom F holds
for x being set st x in F . n holds
a . n = f . x
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 A9; :: 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 set st x in F . n holds
f . x = a . n ) ) by ; :: thesis: verum