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 S_{1}[ 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 S_{1}[k,y]

A9: ( dom a = Seg (len F) & ( for k being Nat st k in Seg (len F) holds

S_{1}[k,a . k] ) )
from FINSEQ_1:sch 5(A3);

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 ) )

for x being set st x in F . n holds

f . x = a . n ) ) by A1, A9, FINSEQ_1:def 3; :: thesis: verum

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 S

$2 = f . x;

A3: for k being Nat st k in Seg (len F) holds

ex y being Element of COMPLEX st S

proof

consider a being FinSequence of COMPLEX such that
let k be Nat; :: thesis: ( k in Seg (len F) implies ex y being Element of COMPLEX st S_{1}[k,y] )

assume k in Seg (len F) ; :: thesis: ex y being Element of COMPLEX st S_{1}[k,y]

then A4: k in dom F by FINSEQ_1:def 3;

then A5: F . k in rng F by FUNCT_1:3;

end;assume k in Seg (len F) ; :: thesis: ex y being Element of COMPLEX st S

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 <> {} )
;

end;

suppose A6:
F . k = {}
; :: thesis: ex y being Element of COMPLEX st S_{1}[k,y]

0 in REAL
by XREAL_0:def 1;

then reconsider y = 0 as Element of COMPLEX by NUMBERS:11;

take y ; :: thesis: S_{1}[k,y]

thus S_{1}[k,y]
by A6; :: thesis: verum

end;then reconsider y = 0 as Element of COMPLEX by NUMBERS:11;

take y ; :: thesis: S

thus S

suppose
F . k <> {}
; :: thesis: ex y being Element of COMPLEX st S_{1}[k,y]

then consider x1 being object such that

A7: x1 in F . k by XBOOLE_0:def 1;

x1 in dom f by A1, A5, A7, TARSKI:def 4;

then f . x1 in rng f by FUNCT_1:3;

then reconsider y = f . x1 as Element of COMPLEX ;

take y ; :: thesis: S_{1}[k,y]

end;A7: x1 in F . k by XBOOLE_0:def 1;

x1 in dom f by A1, A5, A7, TARSKI:def 4;

then f . x1 in rng f by FUNCT_1:3;

then reconsider y = f . x1 as Element of COMPLEX ;

take y ; :: thesis: S

A9: ( dom a = Seg (len F) & ( for k being Nat st k in Seg (len F) holds

S

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

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

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;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

for x being set st x in F . n holds

f . x = a . n ) ) by A1, A9, FINSEQ_1:def 3; :: thesis: verum