let f2, f1 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 A1: 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 )
thus A2: ( rng s c= dom (f2 * f1) & rng s c= X ) by A1, XBOOLE_1:18; :: 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:44;
hence rng s c= dom f1 by A2, XBOOLE_1:1; :: thesis: ( rng s c= (dom f1) /\ X & rng (f1 /* s) c= dom f2 )
hence rng s c= (dom f1) /\ X by A2, XBOOLE_1:19; :: thesis: rng (f1 /* s) c= dom f2
let x be set ; :: 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
A4: (f1 /* s) . n = x by FUNCT_2:190;
s . n in rng s by VALUED_0:28;
then f1 . (s . n) in dom f2 by A2, FUNCT_1:21;
hence x in dom f2 by A2, A3, A4, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum