let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL
for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
let f, g be PartFunc of X,ExtREAL ; :: thesis: for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
let x be set ; :: thesis: ( x in dom |.(f + g).| implies |.(f + g).| . x <= (|.f.| + |.g.|) . x )
assume A1: x in dom |.(f + g).| ; :: thesis: |.(f + g).| . x <= (|.f.| + |.g.|) . x
then A2: x in dom (f + g) by MESFUNC1:def 10;
then x in ((dom f) /\ (dom g)) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by MESFUNC1:def 3;
then ( x in (dom f) /\ (dom g) & not x in ((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty })) ) by XBOOLE_0:def 5;
then A3: ( x in dom f & x in dom g & not x in (f " {-infty }) /\ (g " {+infty }) & not x in (f " {+infty }) /\ (g " {-infty }) ) by XBOOLE_0:def 3, XBOOLE_0:def 4;
then ( ( not x in f " {-infty } or not x in g " {+infty } ) & ( not x in f " {+infty } or not x in g " {-infty } ) ) by XBOOLE_0:def 4;
then ( ( not f . x in {-infty } or not g . x in {+infty } ) & ( not f . x in {+infty } or not g . x in {-infty } ) ) by A3, FUNCT_1:def 13;
then ( ( f . x <> -infty or g . x <> +infty ) & ( f . x <> +infty or g . x <> -infty ) ) by TARSKI:def 1;
then |.((f . x) + (g . x)).| <= |.(f . x).| + |.(g . x).| by EXTREAL2:61;
then A4: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by A2, MESFUNC1:def 3;
A5: ( dom |.(f + g).| c= dom |.f.| & dom |.(f + g).| c= dom |.g.| ) by Th19;
then A6: ( |.(f . x).| = |.f.| . x & |.(g . x).| = |.g.| . x ) by A1, MESFUNC1:def 10;
( x in dom |.f.| & x in dom |.g.| ) by A1, A5;
then ( x in dom f & x in dom g ) by MESFUNC1:def 10;
then x in (dom f) /\ (dom g) by XBOOLE_0:def 4;
then x in dom (|.f.| + |.g.|) by Th19;
then |.(f . x).| + |.(g . x).| = (|.f.| + |.g.|) . x by A6, MESFUNC1:def 3;
hence |.(f + g).| . x <= (|.f.| + |.g.|) . x by A1, A4, MESFUNC1:def 10; :: thesis: verum