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.|;
A1: dom (|.f.| + |.g.|) = ((dom |.f.|) /\ (dom |.g.|)) \ (((|.f.| " {-infty }) /\ (|.g.| " {+infty })) \/ ((|.f.| " {+infty }) /\ (|.g.| " {-infty }))) by MESFUNC1:def 3;
( |.f.| is without-infty & |.g.| is without-infty ) by MESFUNC5:18;
then ( not -infty in rng |.f.| & not -infty in rng |.g.| ) by MESFUNC5:def 3;
then ( |.f.| " {-infty } = {} & |.g.| " {-infty } = {} ) by FUNCT_1:142;
then dom (|.f.| + |.g.|) = (dom f) /\ (dom |.g.|) by A1, 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