let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let f be PartFunc of X,ExtREAL ; :: thesis:
assume that
A1: f is_simple_func_in S and
A2: for x being set st x in dom f holds
0. <= f . x ; :: thesis:

per cases ;

suppose ex x being set st
( x in dom f & 0. = f . x ) ; :: thesis:

hence ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) ) by A1, A2, Lm3; :: thesis:

end;

suppose for x being set st x in dom f holds
0. <> f . x ; :: thesis:

end;