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= X & 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= X & 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= X & rng s c= dom f1 & rng s c= (dom f1) /\ X & rng (f1 /* s) c= dom f2 ) )
assume rng s c= (dom (f2 * f1)) /\ X ; :: thesis: ( rng s c= dom (f2 * f1) & rng s c= X & rng s c= dom f1 & rng s c= (dom f1) /\ X & rng (f1 /* s) c= dom f2 )
hence A1: ( rng s c= dom (f2 * f1) & rng s c= X ) by XBOOLE_1:18; :: thesis: ( rng s c= dom f1 & rng s c= (dom f1) /\ X & rng (f1 /* s) c= dom f2 )
A2: dom (f2 * f1) c= dom f1 by RELAT_1:25;
hence rng s c= dom f1 by A1; :: thesis: ( rng s c= (dom f1) /\ X & rng (f1 /* s) c= dom f2 )
hence rng s c= (dom f1) /\ X by A1, XBOOLE_1:19; :: thesis: rng (f1 /* s) c= dom f2
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
A3: (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 A1, FUNCT_1:11;
hence x in dom f2 by A1, A2, A3, FUNCT_2:108, XBOOLE_1:1; :: thesis: verum