let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,REAL holds
( f is_simple_func_in S iff R_EAL f is_simple_func_in S )
let S be SigmaField of X; :: thesis: for f being PartFunc of X,REAL holds
( f is_simple_func_in S iff R_EAL f is_simple_func_in S )
let f be PartFunc of X,REAL ; :: thesis: ( f is_simple_func_in S iff R_EAL f is_simple_func_in S )

hereby :: thesis: ( R_EAL f is_simple_func_in S implies f is_simple_func_in S )

assume f is_simple_func_in S ; :: thesis: R_EAL f is_simple_func_in S
then consider F being Finite_Sep_Sequence of S such that
A1: ( dom f = union (rng F) & ( 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 ) ) by Def7;
thus R_EAL f is_simple_func_in S by A1, MESFUNC2:def 5; :: thesis: verum

end;

assume R_EAL f is_simple_func_in S ; :: thesis: f is_simple_func_in S
then consider F being Finite_Sep_Sequence of S such that
A2: ( dom (R_EAL f) = union (rng F) & ( 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
(R_EAL f) . x = (R_EAL f) . y ) ) by MESFUNC2:def 5;
thus f is_simple_func_in S by A2, Def7; :: thesis: verum