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 MES312;
( F, Re c are_Re-presentation_of Re f & F, Im c are_Re-presentation_of Im f ) by A1, Def16;
then ( 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 A1, MES3Cdef1, MES3def1;
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 ) ) ; :: thesis: verum

end;

given F being Finite_Sep_Sequence of S, c being FinSequence of COMPLEX such that A1: ( dom f = union (rng F) & dom F = dom c ) and
A2: 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
A3: 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
B1: ( dom (Re f) = union (rng F) & dom (Im f) = union (rng F) ) by A1, MESFUN6C:def 1, MESFUN6C:def 2;
( len (Re c) = len c & len (Im c) = len c ) by COMPLSP2:48;
then ( dom (Re c) = Seg (len c) & dom (Im c) = Seg (len c) ) by FINSEQ_1:def 3;
then B2: ( dom F = dom (Re c) & dom F = dom (Im c) ) by A1, FINSEQ_1: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 P01: 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 P02: x in F . n ; :: thesis: f . x = c . n
P03: F . n c= union (rng F) by P01, MESFUNC3:7;
then x in dom (Re f) by P02, B1;
then P04: (Re f) . x = Re (f . x) by MESFUN6C:def 1;
(Re f) . x = (Re c) . n by P01, P02, A2;
then P05: Re (f . x) = Re (c . n) by P01, B2, Def31, P04;
x in dom (Im f) by P02, P03, B1;
then P06: (Im f) . x = Im (f . x) by MESFUN6C:def 2;
(Im f) . x = (Im c) . n by P01, P02, A3;
then Im (f . x) = Im (c . n) by P01, B2, Def32, P06;
hence f . x = c . n by P05, COMPLEX1:def 5; :: thesis: verum

end;

then F,c are_Re-presentation_of f by A1, MES3Cdef1;
hence f is_simple_func_in S by MES312; :: thesis: verum