let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL holds
( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
let f, g be PartFunc of X,ExtREAL; :: thesis: ( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
set F = |.f.|;
set G = |.g.|;
|.f.| is without-infty by MESFUNC5:12;
then not -infty in rng |.f.| ;
then A1: |.f.| " {-infty} = {} by FUNCT_1:72;
|.g.| is without-infty by MESFUNC5:12;
then not -infty in rng |.g.| ;
then A2: |.g.| " {-infty} = {} by FUNCT_1:72;
dom (|.f.| + |.g.|) = ((dom |.f.|) /\ (dom |.g.|)) \ (((|.f.| " {-infty}) /\ (|.g.| " {+infty})) \/ ((|.f.| " {+infty}) /\ (|.g.| " {-infty}))) by MESFUNC1:def 3;
then dom (|.f.| + |.g.|) = (dom f) /\ (dom |.g.|) by A1, A2, MESFUNC1:def 10;
hence dom (|.f.| + |.g.|) = (dom f) /\ (dom g) by MESFUNC1:def 10; :: thesis: dom |.(f + g).| c= dom |.f.|
dom |.(f + g).| = dom (f + g) by MESFUNC1:def 10
.= ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3
.= (dom f) /\ ((dom g) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty})))) by XBOOLE_1:49 ;
then dom |.(f + g).| c= dom f by XBOOLE_1:17;
hence dom |.(f + g).| c= dom |.f.| by MESFUNC1:def 10; :: thesis: verum