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 () )

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;

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;