let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,REAL st f is_simple_func_in S holds
rng f is bounded
let S be SigmaField of X; :: thesis: for f being PartFunc of X,REAL st f is_simple_func_in S holds
rng f is bounded
let f be PartFunc of X,REAL ; :: thesis: ( f is_simple_func_in S implies rng f is bounded )
assume f is_simple_func_in S ; :: thesis: rng f is bounded
then consider F being Finite_Sep_Sequence of S, a being FinSequence of REAL such that
A1: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) ) by MES33;
rng f c= rng a

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in rng a )
assume y in rng f ; :: thesis: y in rng a
then consider x being set such that
P01: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
consider z being set such that
P02: ( x in z & z in rng F ) by A1, P01, TARSKI:def 4;
consider n being set such that
P03: ( n in dom F & z = F . n ) by P02, FUNCT_1:def 5;
f . x = a . n by A1, P03, P02;
hence y in rng a by P03, A1, FUNCT_1:def 5, P01; :: thesis: verum

end;

hence rng f is bounded by RCOMP_1:28; :: thesis: verum