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 ;
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 ;
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:
A8: dom (Im f) = union (rng F) by ;
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 ;
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 ;
A11: dom (Re f) = union (rng F) by ;
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 ;
then x in dom (Im f) by ;
then A15: (Im f) . x = Im (f . x) by COMSEQ_3:def 4;
x in dom (Re f) by ;
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 ;
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