let seq be Real_Sequence; :: thesis: for f1, f2 being PartFunc of REAL ,REAL
for X being Subset of REAL st rng seq c= (dom (f1 + f2)) /\ X holds
( rng seq c= dom (f1 + f2) & rng seq c= X & dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: for X being Subset of REAL st rng seq c= (dom (f1 + f2)) /\ X holds
( rng seq c= dom (f1 + f2) & rng seq c= X & dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )
let X be Subset of REAL ; :: thesis: ( rng seq c= (dom (f1 + f2)) /\ X implies ( rng seq c= dom (f1 + f2) & rng seq c= X & dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X ) )
assume A1: rng seq c= (dom (f1 + f2)) /\ X ; :: thesis: ( rng seq c= dom (f1 + f2) & rng seq c= X & dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )
( (dom (f1 + f2)) /\ X c= dom (f1 + f2) & (dom (f1 + f2)) /\ X c= X ) by XBOOLE_1:17;
hence A2: ( rng seq c= dom (f1 + f2) & rng seq c= X ) by A1, XBOOLE_1:1; :: thesis: ( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )
thus dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def 1; :: thesis: ( rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )
then ( dom (f1 + f2) c= dom f1 & dom (f1 + f2) c= dom f2 ) by XBOOLE_1:17;
then ( rng seq c= dom f1 & rng seq c= dom f2 ) by A2, XBOOLE_1:1;
hence ( rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X ) by A2, XBOOLE_1:19; :: thesis: verum