let X, Y be set ; :: thesis: for r being Real
for h1, h2 being PartFunc of REAL,REAL st r in (X /\ Y) /\ (dom (h1 + h2)) holds
( r in X /\ (dom h1) & r in Y /\ (dom h2) )
let r be Real; :: thesis: for h1, h2 being PartFunc of REAL,REAL st r in (X /\ Y) /\ (dom (h1 + h2)) holds
( r in X /\ (dom h1) & r in Y /\ (dom h2) )
let h1, h2 be PartFunc of REAL,REAL; :: thesis: ( r in (X /\ Y) /\ (dom (h1 + h2)) implies ( r in X /\ (dom h1) & r in Y /\ (dom h2) ) )
assume A1: r in (X /\ Y) /\ (dom (h1 + h2)) ; :: thesis: ( r in X /\ (dom h1) & r in Y /\ (dom h2) )
then r in dom (h1 + h2) by XBOOLE_0:def 4;
then r in (dom h1) /\ (dom h2) by VALUED_1:def 1;
then A2: ( r in dom h1 & r in dom h2 ) by XBOOLE_0:def 4;
r in X /\ Y by A1, XBOOLE_0:def 4;
then ( r in X & r in Y ) by XBOOLE_0:def 4;
hence ( r in X /\ (dom h1) & r in Y /\ (dom h2) ) by A2, XBOOLE_0:def 4; :: thesis: verum