let x0 be Real; for S being RealNormSpace
for f1 being PartFunc of REAL,S
for f2 being PartFunc of S,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 S be RealNormSpace; for f1 being PartFunc of REAL,S
for f2 being PartFunc of S,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 be PartFunc of REAL,S; for f2 being PartFunc of S,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 be PartFunc of S,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 ( not rng s1 c= dom (f2 * f1) or not s1 is convergent or not lim s1 = x0 or ( (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;
A7:
rng (f1 /* s1) c= dom f2
then A11:
f2 /* (f1 /* s1) = (f2 * f1) /* s1
by FUNCT_2:63;
rng s1 c= dom f1
by A4, A6;
then A12:
( f1 /* s1 is convergent & f1 /. x0 = lim (f1 /* s1) )
by A2, A5;
hence
(f2 * f1) /* s1 is convergent
by A3, A7, A11, NFCONT_1:def 6; (f2 * f1) . x0 = lim ((f2 * f1) /* s1)
thus (f2 * f1) . x0 =
(f2 * f1) /. x0
by A1, PARTFUN1:def 6
.=
f2 /. (f1 /. x0)
by A1, PARTFUN2:3
.=
lim (f2 /* (f1 /* s1))
by A12, A3, A7, NFCONT_1:def 6
.=
lim ((f2 * f1) /* s1)
by A9, FUNCT_2:63
; verum