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 r being Real st dom f in S & 0 <= r & ( for x being object st x in dom f holds

f . x = r ) holds

integral' (M,f) = r * (M . (dom f))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for r being Real st dom f in S & 0 <= r & ( for x being object st x in dom f holds

f . x = r ) holds

integral' (M,f) = r * (M . (dom f))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for r being Real st dom f in S & 0 <= r & ( for x being object st x in dom f holds

f . x = r ) holds

integral' (M,f) = r * (M . (dom f))

let f be PartFunc of X,ExtREAL; :: thesis: for r being Real st dom f in S & 0 <= r & ( for x being object st x in dom f holds

f . x = r ) holds

integral' (M,f) = r * (M . (dom f))

let r be Real; :: thesis: ( dom f in S & 0 <= r & ( for x being object st x in dom f holds

f . x = r ) implies integral' (M,f) = r * (M . (dom f)) )

assume that

A1: dom f in S and

A2: 0 <= r and

A3: for x being object st x in dom f holds

f . x = r ; :: thesis: integral' (M,f) = r * (M . (dom f))

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for r being Real st dom f in S & 0 <= r & ( for x being object st x in dom f holds

f . x = r ) holds

integral' (M,f) = r * (M . (dom f))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for r being Real st dom f in S & 0 <= r & ( for x being object st x in dom f holds

f . x = r ) holds

integral' (M,f) = r * (M . (dom f))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for r being Real st dom f in S & 0 <= r & ( for x being object st x in dom f holds

f . x = r ) holds

integral' (M,f) = r * (M . (dom f))

let f be PartFunc of X,ExtREAL; :: thesis: for r being Real st dom f in S & 0 <= r & ( for x being object st x in dom f holds

f . x = r ) holds

integral' (M,f) = r * (M . (dom f))

let r be Real; :: thesis: ( dom f in S & 0 <= r & ( for x being object st x in dom f holds

f . x = r ) implies integral' (M,f) = r * (M . (dom f)) )

assume that

A1: dom f in S and

A2: 0 <= r and

A3: for x being object st x in dom f holds

f . x = r ; :: thesis: integral' (M,f) = r * (M . (dom f))