let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let f be PartFunc of X,REAL; :: thesis:
assume f is_simple_func_in S ; :: thesis:
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

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
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:

end;