let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is nonnegative & g is nonnegative holds

f + g is nonnegative

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

for f, g being PartFunc of X,ExtREAL st f is nonnegative & g is nonnegative holds

f + g is nonnegative

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is nonnegative & g is nonnegative holds

f + g is nonnegative

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is nonnegative & g is nonnegative implies f + g is nonnegative )

assume that

A1: f is nonnegative and

A2: g is nonnegative ; :: thesis: f + g is nonnegative

for x being object st x in dom (f + g) holds

0 <= (f + g) . x

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is nonnegative & g is nonnegative holds

f + g is nonnegative

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

for f, g being PartFunc of X,ExtREAL st f is nonnegative & g is nonnegative holds

f + g is nonnegative

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is nonnegative & g is nonnegative holds

f + g is nonnegative

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is nonnegative & g is nonnegative implies f + g is nonnegative )

assume that

A1: f is nonnegative and

A2: g is nonnegative ; :: thesis: f + g is nonnegative

for x being object st x in dom (f + g) holds

0 <= (f + g) . x

proof

hence
f + g is nonnegative
by SUPINF_2:52; :: thesis: verum
let x be object ; :: thesis: ( x in dom (f + g) implies 0 <= (f + g) . x )

assume A3: x in dom (f + g) ; :: thesis: 0 <= (f + g) . x

0 <= f . x by A1, SUPINF_2:51;

then A4: g . x <= (f . x) + (g . x) by XXREAL_3:39;

0 <= g . x by A2, SUPINF_2:51;

hence 0 <= (f + g) . x by A3, A4, MESFUNC1:def 3; :: thesis: verum

end;assume A3: x in dom (f + g) ; :: thesis: 0 <= (f + g) . x

0 <= f . x by A1, SUPINF_2:51;

then A4: g . x <= (f . x) + (g . x) by XXREAL_3:39;

0 <= g . x by A2, SUPINF_2:51;

hence 0 <= (f + g) . x by A3, A4, MESFUNC1:def 3; :: thesis: verum