let f1, f2 be PartFunc of REAL,REAL; :: thesis: for s being Real_Sequence
for X being set st rng s c= (dom (f2 * f1)) \ X holds
( rng s c= dom (f2 * f1) & rng s c= dom f1 & rng s c= (dom f1) \ X & rng (f1 /* s) c= dom f2 )
let s be Real_Sequence; :: thesis: for X being set st rng s c= (dom (f2 * f1)) \ X holds
( rng s c= dom (f2 * f1) & rng s c= dom f1 & rng s c= (dom f1) \ X & rng (f1 /* s) c= dom f2 )
let X be set ; :: thesis: ( rng s c= (dom (f2 * f1)) \ X implies ( rng s c= dom (f2 * f1) & rng s c= dom f1 & rng s c= (dom f1) \ X & rng (f1 /* s) c= dom f2 ) )
assume A1: rng s c= (dom (f2 * f1)) \ X ; :: thesis: ( rng s c= dom (f2 * f1) & rng s c= dom f1 & rng s c= (dom f1) \ X & rng (f1 /* s) c= dom f2 )
(dom (f2 * f1)) \ X c= dom (f2 * f1) by XBOOLE_1:36;
hence A2: rng s c= dom (f2 * f1) by A1; :: thesis: ( rng s c= dom f1 & rng s c= (dom f1) \ X & rng (f1 /* s) c= dom f2 )
A3: dom (f2 * f1) c= dom f1 by RELAT_1:25;
hence A4: rng s c= dom f1 by A2; :: thesis: ( rng s c= (dom f1) \ X & rng (f1 /* s) c= dom f2 )
thus rng s c= (dom f1) \ X :: thesis: rng (f1 /* s) c= dom f2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng s or x in (dom f1) \ X )
assume A5: x in rng s ; :: thesis: x in (dom f1) \ X
then not x in X by A1, XBOOLE_0:def 5;
hence x in (dom f1) \ X by A4, A5, XBOOLE_0:def 5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f1 /* s) or x in dom f2 )
assume x in rng (f1 /* s) ; :: thesis: x in dom f2
then consider n being Element of NAT such that
A6: (f1 /* s) . n = x by FUNCT_2:113;
s . n in rng s by VALUED_0:28;
then f1 . (s . n) in dom f2 by A2, FUNCT_1:11;
hence x in dom f2 by A2, A3, A6, FUNCT_2:108, XBOOLE_1:1; :: thesis: verum