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 & 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 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 & rng seq c= 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 & 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) & rng seq c= X & 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 )
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; :: 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 A4: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def 4; :: thesis: ( rng seq c= dom f1 & rng seq c= dom f2 & rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )
then A5: dom (f1 (#) f2) c= dom f2 by XBOOLE_1:17;
dom (f1 (#) f2) c= dom f1 by A4, XBOOLE_1:17;
hence ( rng seq c= dom f1 & rng seq c= dom f2 ) by A3, A5, XBOOLE_1:1; :: thesis: ( rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X )
hence ( rng seq c= (dom f1) /\ X & rng seq c= (dom f2) /\ X ) by A3, XBOOLE_1:19; :: thesis: verum