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 A1, MESFUNC2:def 4;

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 A1, MESFUNC2:def 4;

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

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