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 A4: dom (f1 + f2) c= dom f2 by XBOOLE_1:17;
dom (f1 + f2) c= dom f1 by A3, XBOOLE_1:17;
hence ( rng seq c= dom f1 & rng seq c= dom f2 ) by A2, A4; :: thesis: ( rng seq c= (dom f1) \ X & rng seq c= (dom f2) \ X )
A5: (dom (f1 + f2)) \ X c= (dom f2) \ X by A3, XBOOLE_1:17, XBOOLE_1:33;
(dom (f1 + f2)) \ X c= (dom f1) \ X by A3, XBOOLE_1:17, XBOOLE_1:33;
hence ( rng seq c= (dom f1) \ X & rng seq c= (dom f2) \ X ) by A1, A5; :: thesis: verum