let x0 be Real; for f1, f2 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 f1, f2 be PartFunc of REAL,REAL; ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 . x0 implies f2 * f1 is_continuous_in x0 )
assume A1:
x0 in dom (f2 * f1)
; ( not f1 is_continuous_in x0 or not f2 is_continuous_in f1 . x0 or f2 * f1 is_continuous_in x0 )
assume that
A2:
f1 is_continuous_in x0
and
A3:
f2 is_continuous_in f1 . x0
; f2 * f1 is_continuous_in x0
let s1 be Real_Sequence; FCONT_1:def 1 ( 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 that
A4:
rng s1 c= dom (f2 * f1)
and
A5:
( s1 is convergent & lim s1 = x0 )
; ( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) )
A6:
dom (f2 * f1) c= dom f1
by RELAT_1:25;
then A8:
rng (f1 /* s1) c= dom f2
;
then A10:
f2 /* (f1 /* s1) = (f2 * f1) /* s1
by FUNCT_2:63;
rng s1 c= dom f1
by A4, A6;
then A11:
( f1 /* s1 is convergent & f1 . x0 = lim (f1 /* s1) )
by A2, A5;
then
f2 . (f1 . x0) = lim (f2 /* (f1 /* s1))
by A3, A8;
hence
( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) )
by A1, A3, A11, A8, A10, FUNCT_1:12; verum