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

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 )

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;

given F being Finite_Sep_Sequence of S, c being FinSequence of COMPLEX such that A4: dom f = union (rng F) and
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

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;

then F,c are_Re-presentation_of f by A4, A5;
hence f is_simple_func_in S by Th45; :: thesis: verum