let S, T be RealNormSpace; for f1 being PartFunc of S,REAL
for f2 being PartFunc of REAL,T
for x0 being Point of S 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 S,REAL; for f2 being PartFunc of REAL,T
for x0 being Point of S 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 REAL,T; for x0 being Point of S 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 x0 be Point of S; ( 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
thus
x0 in dom (f2 * f1)
by A1; NFCONT_1:def 5 for b1 being Element of K16(K17(NAT, the carrier of S)) holds
( not rng b1 c= dom (f2 * f1) or not b1 is convergent or not lim b1 = x0 or ( (f2 * f1) /* b1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* b1) ) )
let s1 be sequence of S; ( 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;
then A8:
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;
(f2 * f1) /. x0 =
f2 /. (f1 /. x0)
by A1, PARTFUN2:3
.=
lim (f2 /* (f1 /* s1))
by A12, A3, A8, NFCONT_3:def 1
.=
lim ((f2 * f1) /* s1)
by A9, FUNCT_2:63
;
hence
( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) )
by A3, A12, A8, A11, NFCONT_3:def 1; verum