let seq be Real_Sequence; 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; 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; ( 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
; ( 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 )
A2:
(dom (f1 + f2)) /\ X c= X
by XBOOLE_1:17;
(dom (f1 + f2)) /\ X c= dom (f1 + f2)
by XBOOLE_1:17;
hence A3:
( rng seq c= dom (f1 + f2) & rng seq c= X )
by A1, A2, XBOOLE_1:1; ( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )
thus A4:
dom (f1 + f2) = (dom f1) /\ (dom f2)
by VALUED_1:def 1; ( rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )
then
dom (f1 + f2) c= dom f2
by XBOOLE_1:17;
then A5:
rng seq c= dom f2
by A3, XBOOLE_1:1;
dom (f1 + f2) c= dom f1
by A4, XBOOLE_1:17;
then
rng seq c= dom f1
by A3, XBOOLE_1:1;
hence
( rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )
by A3, A5, XBOOLE_1:19; verum