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