let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL st f is () & g is () holds

dom (f - g) = (dom f) /\ (dom g)

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is () & g is () implies dom (f - g) = (dom f) /\ (dom g) )

assume that

A1: f is () and

A2: g is () ; :: thesis: dom (f - g) = (dom f) /\ (dom g)

not +infty in rng g by A2;

then A3: g " {+infty} = {} by FUNCT_1:72;

not -infty in rng f by A1;

then f " {-infty} = {} by FUNCT_1:72;

then ((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty})) = {} by A3;

then dom (f - g) = ((dom f) /\ (dom g)) \ {} by MESFUNC1:def 4;

hence dom (f - g) = (dom f) /\ (dom g) ; :: thesis: verum

dom (f - g) = (dom f) /\ (dom g)

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is () & g is () implies dom (f - g) = (dom f) /\ (dom g) )

assume that

A1: f is () and

A2: g is () ; :: thesis: dom (f - g) = (dom f) /\ (dom g)

not +infty in rng g by A2;

then A3: g " {+infty} = {} by FUNCT_1:72;

not -infty in rng f by A1;

then f " {-infty} = {} by FUNCT_1:72;

then ((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty})) = {} by A3;

then dom (f - g) = ((dom f) /\ (dom g)) \ {} by MESFUNC1:def 4;

hence dom (f - g) = (dom f) /\ (dom g) ; :: thesis: verum