let X, Y be set ; :: thesis: for r being Element of 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 Element of 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 r in (X /\ Y) /\ (dom (h1 + h2)) ; :: thesis: ( r in X /\ (dom h1) & r in Y /\ (dom h2) )
then ( r in X /\ Y & r in dom (h1 + h2) ) by XBOOLE_0:def 4;
then ( r in X & r in Y & r in (dom h1) /\ (dom h2) ) by VALUED_1:def 1, XBOOLE_0:def 4;
then ( r in X & r in Y & r in dom h1 & r in dom h2 ) by XBOOLE_0:def 4;
hence ( r in X /\ (dom h1) & r in Y /\ (dom h2) ) by XBOOLE_0:def 4; :: thesis: verum