let seq be Real_Sequence; :: thesis: for f1, f2 being PartFunc of REAL ,REAL
for X being set st rng seq c= (dom (f1 + f2)) \ X holds
( rng seq c= dom (f1 + f2) & dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= 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 set st rng seq c= (dom (f1 + f2)) \ X holds
( rng seq c= dom (f1 + f2) & dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 & rng seq c= (dom f1) \ X & rng seq c= (dom f2) \ X )
let X be set ; :: thesis: ( rng seq c= (dom (f1 + f2)) \ X implies ( rng seq c= dom (f1 + f2) & dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= 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) & dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 & rng seq c= (dom f1) \ X & rng seq c= (dom f2) \ X )
hence A2: rng seq c= dom (f1 + f2) by XBOOLE_1:1; :: thesis: ( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 & rng seq c= (dom f1) \ X & rng seq c= (dom f2) \ X )
thus A3: dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def 1; :: thesis: ( rng seq c= dom f1 & rng seq c= dom f2 & 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;
hence ( rng seq c= dom f1 & rng seq c= dom f2 ) by A2, XBOOLE_1:1; :: thesis: ( rng seq c= (dom f1) \ X & rng seq c= (dom f2) \ X )
( (dom (f1 + f2)) \ X c= (dom f1) \ X & (dom (f1 + f2)) \ X c= (dom f2) \ X ) by A3, XBOOLE_1:17, XBOOLE_1:33;
hence ( rng seq c= (dom f1) \ X & rng seq c= (dom f2) \ X ) by A1, XBOOLE_1:1; :: thesis: verum