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 real-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 real-bounded
let f be PartFunc of X,REAL; :: thesis: ( f is_simple_func_in S implies rng f is real-bounded )
assume f is_simple_func_in S ; :: thesis: rng f is real-bounded
then consider F being Finite_Sep_Sequence of S, a being FinSequence of REAL such that
A1: dom f = union (rng F) and
A2: dom F = dom a and
A3: 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 Lm2;
rng f c= rng a

proof

let y be object ; :: 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 object such that
A4: x in dom f and
A5: y = f . x by FUNCT_1:def 3;
consider z being set such that
A6: x in z and
A7: z in rng F by A1, A4, TARSKI:def 4;
consider n being object such that
A8: n in dom F and
A9: z = F . n by A7, FUNCT_1:def 3;
f . x = a . n by A3, A6, A8, A9;
hence y in rng a by A2, A5, A8, FUNCT_1:def 3; :: thesis: verum

end;

hence rng f is real-bounded by RCOMP_1:10; :: thesis: verum