let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

dom f is Element of S

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

dom f is Element of S

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

dom f is Element of S

let f be PartFunc of X,ExtREAL; :: 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 MESFUNC2:def 4;

hence dom f is Element of S by MESFUNC2:31; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

dom f is Element of S

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

dom f is Element of S

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

dom f is Element of S

let f be PartFunc of X,ExtREAL; :: 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 MESFUNC2:def 4;

hence dom f is Element of S by MESFUNC2:31; :: thesis: verum