let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds
dom f is Element of S
let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds
dom f is Element of S
let f be PartFunc of X,COMPLEX ; :: thesis: ( f is_simple_func_in S implies dom f is Element of S )
assume f is_simple_func_in S ; :: thesis: dom f is Element of S
then ex F being Finite_Sep_Sequence of S st
( 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 MESFUN7C:def 13;
hence dom f is Element of S by MESFUNC2:34; :: thesis: verum