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 without+infty & f is without-infty )
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
( f is without+infty & f is without-infty )
let f be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S implies ( f is without+infty & f is without-infty ) )
assume A1: f is_simple_func_in S ; :: thesis: ( f is without+infty & f is without-infty )

hereby :: thesis: f is without-infty

assume not f is without+infty ; :: thesis: contradiction
then +infty in rng f by Def4;
then f " {+infty} <> {} by FUNCT_1:142;
then consider x being set such that
A2: x in f " {+infty} by XBOOLE_0:def 1;
A3: f is V55() by A1, MESFUNC2:def 5;
f . x in {+infty} by A2, FUNCT_1:def 13;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum

end;

hereby :: thesis: verum

assume not f is without-infty ; :: thesis: contradiction
then -infty in rng f by Def3;
then f " {-infty} <> {} by FUNCT_1:142;
then consider x being set such that
A4: x in f " {-infty} by XBOOLE_0:def 1;
A5: f is V55() by A1, MESFUNC2:def 5;
f . x in {-infty} by A4, FUNCT_1:def 13;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum

end;