let x0 be real number ; :: thesis: for f2, f1 being PartFunc of REAL ,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 . x0 holds
f2 * f1 is_continuous_in x0
let f2, f1 be PartFunc of REAL ,REAL ; :: thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 . x0 implies f2 * f1 is_continuous_in x0 )
assume Z: x0 in dom (f2 * f1) ; :: thesis: ( not f1 is_continuous_in x0 or not f2 is_continuous_in f1 . x0 or f2 * f1 is_continuous_in x0 )
assume A1: ( f1 is_continuous_in x0 & f2 is_continuous_in f1 . x0 ) ; :: thesis: f2 * f1 is_continuous_in x0
let s1 be Real_Sequence; :: according to FCONT_1:def 1 :: thesis: ( rng s1 c= dom (f2 * f1) & s1 is convergent & lim s1 = x0 implies ( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) ) )
assume A4: ( rng s1 c= dom (f2 * f1) & s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) )
A5: dom (f2 * f1) c= dom f1 by RELAT_1:44;
then rng s1 c= dom f1 by A4, XBOOLE_1:1;
then A6: ( f1 /* s1 is convergent & f1 . x0 = lim (f1 /* s1) ) by A1, A4, Def1;

now

let x be set ; :: thesis: ( x in rng (f1 /* s1) implies x in dom f2 )
assume x in rng (f1 /* s1) ; :: thesis: x in dom f2
then consider n being Element of NAT such that
A7: x = (f1 /* s1) . n by FUNCT_2:190;
s1 . n in rng s1 by VALUED_0:28;
then f1 . (s1 . n) in dom f2 by A4, FUNCT_1:21;
hence x in dom f2 by A4, A5, A7, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

then A8: rng (f1 /* s1) c= dom f2 by TARSKI:def 3;
then A9: ( f2 /* (f1 /* s1) is convergent & f2 . (f1 . x0) = lim (f2 /* (f1 /* s1)) ) by A1, A6, Def1;
f2 /* (f1 /* s1) = (f2 * f1) /* s1

proof

now

let n be Element of NAT ; :: thesis: ((f2 * f1) /* s1) . n = (f2 /* (f1 /* s1)) . n
s1 . n in rng s1 by VALUED_0:28;
then A10: ( s1 . n in dom f1 & f1 . (s1 . n) in dom f2 ) by A4, FUNCT_1:21;
thus ((f2 * f1) /* s1) . n = (f2 * f1) . (s1 . n) by A4, FUNCT_2:185
.= f2 . (f1 . (s1 . n)) by A10, FUNCT_1:23
.= f2 . ((f1 /* s1) . n) by A4, A5, FUNCT_2:185, XBOOLE_1:1
.= (f2 /* (f1 /* s1)) . n by A8, FUNCT_2:185 ; :: thesis: verum

end;

hence f2 /* (f1 /* s1) = (f2 * f1) /* s1 by FUNCT_2:113; :: thesis: verum

end;

hence ( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) ) by Z, A9, FUNCT_1:22; :: thesis: verum