let X be non empty set ; :: thesis: for S being SigmaField of X

for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) ) )

let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) ) )

let f be PartFunc of X,COMPLEX; :: thesis: ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) ) )

A5: dom F = dom c and

A6: for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n and

A7: for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ; :: thesis: f is_simple_func_in S

A8: dom (Im f) = union (rng F) by A4, COMSEQ_3:def 4;

len (Im c) = len c by COMPLSP2:48;

then dom (Im c) = Seg (len c) by FINSEQ_1:def 3;

then A9: dom F = dom (Im c) by A5, FINSEQ_1:def 3;

len (Re c) = len c by COMPLSP2:48;

then dom (Re c) = Seg (len c) by FINSEQ_1:def 3;

then A10: dom F = dom (Re c) by A5, FINSEQ_1:def 3;

A11: dom (Re f) = union (rng F) by A4, COMSEQ_3:def 3;

for n being Nat st n in dom F holds

for x being set st x in F . n holds

f . x = c . n

hence f is_simple_func_in S by Th45; :: thesis: verum

for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) ) )

let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) ) )

let f be PartFunc of X,COMPLEX; :: thesis: ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) ) )

hereby :: thesis: ( ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) ) implies f is_simple_func_in S )

given F being Finite_Sep_Sequence of S, c being FinSequence of COMPLEX such that A4:
dom f = union (rng F)
and ( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) ) implies f is_simple_func_in S )

assume
f is_simple_func_in S
; :: thesis: ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) )

then consider F being Finite_Sep_Sequence of S, c being FinSequence of COMPLEX such that

A1: F,c are_Re-presentation_of f by Th45;

F, Im c are_Re-presentation_of Im f by A1, Th48;

then A2: for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ;

F, Re c are_Re-presentation_of Re f by A1, Th48;

then A3: for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ;

( dom f = union (rng F) & dom F = dom c ) by A1;

hence ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) ) by A3, A2; :: thesis: verum

end;( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) )

then consider F being Finite_Sep_Sequence of S, c being FinSequence of COMPLEX such that

A1: F,c are_Re-presentation_of f by Th45;

F, Im c are_Re-presentation_of Im f by A1, Th48;

then A2: for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ;

F, Re c are_Re-presentation_of Re f by A1, Th48;

then A3: for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ;

( dom f = union (rng F) & dom F = dom c ) by A1;

hence ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) ) by A3, A2; :: thesis: verum

A5: dom F = dom c and

A6: for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n and

A7: for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ; :: thesis: f is_simple_func_in S

A8: dom (Im f) = union (rng F) by A4, COMSEQ_3:def 4;

len (Im c) = len c by COMPLSP2:48;

then dom (Im c) = Seg (len c) by FINSEQ_1:def 3;

then A9: dom F = dom (Im c) by A5, FINSEQ_1:def 3;

len (Re c) = len c by COMPLSP2:48;

then dom (Re c) = Seg (len c) by FINSEQ_1:def 3;

then A10: dom F = dom (Re c) by A5, FINSEQ_1:def 3;

A11: dom (Re f) = union (rng F) by A4, COMSEQ_3:def 3;

for n being Nat st n in dom F holds

for x being set st x in F . n holds

f . x = c . n

proof

then
F,c are_Re-presentation_of f
by A4, A5;
let n be Nat; :: thesis: ( n in dom F implies for x being set st x in F . n holds

f . x = c . n )

assume A12: n in dom F ; :: thesis: for x being set st x in F . n holds

f . x = c . n

let x be set ; :: thesis: ( x in F . n implies f . x = c . n )

assume A13: x in F . n ; :: thesis: f . x = c . n

A14: F . n c= union (rng F) by A12, MESFUNC3:7;

then x in dom (Im f) by A8, A13;

then A15: (Im f) . x = Im (f . x) by COMSEQ_3:def 4;

x in dom (Re f) by A11, A13, A14;

then A16: (Re f) . x = Re (f . x) by COMSEQ_3:def 3;

(Im f) . x = (Im c) . n by A7, A12, A13;

then A17: Im (f . x) = Im (c . n) by A9, A12, A15, Th47;

(Re f) . x = (Re c) . n by A6, A12, A13;

then Re (f . x) = Re (c . n) by A10, A12, A16, Th46;

hence f . x = c . n by A17; :: thesis: verum

end;f . x = c . n )

assume A12: n in dom F ; :: thesis: for x being set st x in F . n holds

f . x = c . n

let x be set ; :: thesis: ( x in F . n implies f . x = c . n )

assume A13: x in F . n ; :: thesis: f . x = c . n

A14: F . n c= union (rng F) by A12, MESFUNC3:7;

then x in dom (Im f) by A8, A13;

then A15: (Im f) . x = Im (f . x) by COMSEQ_3:def 4;

x in dom (Re f) by A11, A13, A14;

then A16: (Re f) . x = Re (f . x) by COMSEQ_3:def 3;

(Im f) . x = (Im c) . n by A7, A12, A13;

then A17: Im (f . x) = Im (c . n) by A9, A12, A15, Th47;

(Re f) . x = (Re c) . n by A6, A12, A13;

then Re (f . x) = Re (c . n) by A10, A12, A16, Th46;

hence f . x = c . n by A17; :: thesis: verum

hence f is_simple_func_in S by Th45; :: thesis: verum