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 a being FinSequence of COMPLEX st F,a are_Re-presentation_of f )
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 a being FinSequence of COMPLEX st F,a are_Re-presentation_of f )
let f be PartFunc of X,COMPLEX ; :: thesis: ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f )

hereby :: thesis: ( ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f implies f is_simple_func_in S )

assume f is_simple_func_in S ; :: thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f
then consider F being Finite_Sep_Sequence of S, a being FinSequence of COMPLEX such that
A1: ( 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 ) ) by MES33A;
take F = F; :: thesis: ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f
take a = a; :: thesis: F,a are_Re-presentation_of f
thus F,a are_Re-presentation_of f by A1, MES3Cdef1; :: thesis: verum

end;

given F being Finite_Sep_Sequence of S, a being FinSequence of COMPLEX such that A1: F,a are_Re-presentation_of f ; :: thesis: f is_simple_func_in S
A2: ( 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 ) ) by A1, MES3Cdef1;
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

proof

let n be Nat; :: thesis: 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
let x, y be Element of X; :: thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y )
assume ( n in dom F & x in F . n & y in F . n ) ; :: thesis: f . x = f . y
then ( f . x = a . n & f . y = a . n ) by A1, MES3Cdef1;
hence f . x = f . y ; :: thesis: verum

end;

hence f is_simple_func_in S by A2, MES2def5; :: thesis: verum