let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL st f is without-infty & g is without-infty holds
dom (f + g) = (dom f) /\ (dom g)
let f, g be PartFunc of X,ExtREAL ; :: thesis: ( f is without-infty & g is without-infty implies dom (f + g) = (dom f) /\ (dom g) )
assume that
A1: f is without-infty and
A2: g is without-infty ; :: thesis: dom (f + g) = (dom f) /\ (dom g)
not -infty in rng g by A2, Def3;
then A3: g " {-infty } = {} by FUNCT_1:142;
not -infty in rng f by A1, Def3;
then f " {-infty } = {} by FUNCT_1:142;
then ((f " {+infty }) /\ (g " {-infty })) \/ ((f " {-infty }) /\ (g " {+infty })) = {} by A3;
then dom (f + g) = ((dom f) /\ (dom g)) \ {} by MESFUNC1:def 3;
hence dom (f + g) = (dom f) /\ (dom g) ; :: thesis: verum