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 V55() by ;
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 ;
hence a . n is Real by A4; :: thesis: verum
end;
hence ( F . n = {} or a . n is Real ) ; :: thesis: verum