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

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

( f is () & f is () )

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

( f is () & f is () )

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S implies ( f is () & f is () ) )

assume A1: f is_simple_func_in S ; :: thesis: ( f is () & f is () )

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

( f is () & f is () )

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

( f is () & f is () )

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S implies ( f is () & f is () ) )

assume A1: f is_simple_func_in S ; :: thesis: ( f is () & f is () )

hereby :: thesis: f is ()

assume
f is ()
; :: thesis: contradiction

then +infty in rng f ;

then f " {+infty} <> {} by FUNCT_1:72;

then consider x being object such that

A2: x in f " {+infty} by XBOOLE_0:def 1;

A3: f is real-valued by A1, MESFUNC2:def 4;

f . x in {+infty} by A2, FUNCT_1:def 7;

hence contradiction by A3, TARSKI:def 1; :: thesis: verum

end;then +infty in rng f ;

then f " {+infty} <> {} by FUNCT_1:72;

then consider x being object such that

A2: x in f " {+infty} by XBOOLE_0:def 1;

A3: f is real-valued by A1, MESFUNC2:def 4;

f . x in {+infty} by A2, FUNCT_1:def 7;

hence contradiction by A3, TARSKI:def 1; :: thesis: verum

hereby :: thesis: verum

assume
f is ()
; :: thesis: contradiction

then -infty in rng f ;

then f " {-infty} <> {} by FUNCT_1:72;

then consider x being object such that

A4: x in f " {-infty} by XBOOLE_0:def 1;

A5: f is real-valued by A1, MESFUNC2:def 4;

f . x in {-infty} by A4, FUNCT_1:def 7;

hence contradiction by A5, TARSKI:def 1; :: thesis: verum

end;then -infty in rng f ;

then f " {-infty} <> {} by FUNCT_1:72;

then consider x being object such that

A4: x in f " {-infty} by XBOOLE_0:def 1;

A5: f is real-valued by A1, MESFUNC2:def 4;

f . x in {-infty} by A4, FUNCT_1:def 7;

hence contradiction by A5, TARSKI:def 1; :: thesis: verum