let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for n being Nat st f is_simple_func_in S & F,a are_Re-presentation_of f & n in dom F & not F . n = {} holds
a . n is Real
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for n being Nat st f is_simple_func_in S & F,a are_Re-presentation_of f & n in dom F & not F . n = {} holds
a . n is Real
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for n being Nat st f is_simple_func_in S & F,a are_Re-presentation_of f & n in dom F & not F . n = {} holds
a . n is Real
let f be PartFunc of X,ExtREAL; :: thesis: for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for n being Nat st f is_simple_func_in S & F,a are_Re-presentation_of f & n in dom F & not F . n = {} holds
a . n is Real
let F be Finite_Sep_Sequence of S; :: thesis: for a being FinSequence of ExtREAL
for n being Nat st f is_simple_func_in S & F,a are_Re-presentation_of f & n in dom F & not F . n = {} holds
a . n is Real
let a be FinSequence of ExtREAL ; :: thesis: for n being Nat st f is_simple_func_in S & F,a are_Re-presentation_of f & n in dom F & not F . n = {} holds
a . n is Real
let n be Nat; :: thesis: ( f is_simple_func_in S & F,a are_Re-presentation_of f & n in dom F & not F . n = {} implies a . n is Real )
assume that
A1: f is_simple_func_in S and
A2: F,a are_Re-presentation_of f and
A3: n in dom F ; :: thesis: ( F . n = {} or a . n is Real )
A4: f is real-valued by A1, MESFUNC2:def 4;

now :: thesis: ( F . n <> {} implies a . n is Real )

assume F . n <> {} ; :: thesis: a . n is Real
then consider x being object such that
A5: x in F . n by XBOOLE_0:def 1;
a . n = f . x by A2, A3, A5, MESFUNC3:def 1;
hence a . n is Real by A4; :: thesis: verum

end;

hence ( F . n = {} or a . n is Real ) ; :: thesis: verum