set X = dom f;
A1:
dom f c= dom (r (#) f)
by VALUED_1:def 5;
A2:
f | (dom f) is continuous
;
A3:
now for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 in dom f holds
( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) )let s1 be
Real_Sequence;
( rng s1 c= dom f & s1 is convergent & lim s1 in dom f implies ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) ) )assume that A4:
rng s1 c= dom f
and A5:
s1 is
convergent
and A6:
lim s1 in dom f
;
( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) )A7:
f /* s1 is
convergent
by A2, A4, A5, A6, Th13;
then A8:
r (#) (f /* s1) is
convergent
;
f . (lim s1) = lim (f /* s1)
by A2, A4, A5, A6, Th13;
then (r (#) f) . (lim s1) =
r * (lim (f /* s1))
by A1, A6, VALUED_1:def 5
.=
lim (r (#) (f /* s1))
by A7, SEQ_2:8
.=
lim ((r (#) f) /* s1)
by A4, RFUNCT_2:9
;
hence
(
(r (#) f) /* s1 is
convergent &
(r (#) f) . (lim s1) = lim ((r (#) f) /* s1) )
by A4, A8, RFUNCT_2:9;
verum end;
dom (r (#) f) = dom f
by VALUED_1:def 5;
then
(r (#) f) | (dom f) = r (#) f
;
hence
for b1 being PartFunc of REAL,REAL st b1 = r (#) f holds
b1 is continuous
by A1, A3, Th13; verum