set X = dom f;
A1: dom f = dom (r (#) f) by VFUNCT_1:def 4;
then A2: (r (#) f) | (dom f) = r (#) f ;

now :: thesis: 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; :: thesis: ( 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
A3: rng s1 c= dom f and
A4: s1 is convergent and
A5: lim s1 in dom f ; :: thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) )
f | (dom f) is continuous ;
then A6: ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) by A3, A4, A5, Th16;
then A7: r * (f /* s1) is convergent by NORMSP_1:22;
(r (#) f) /. (lim s1) = r * (lim (f /* s1)) by A1, A5, A6, VFUNCT_1:def 4
.= lim (r * (f /* s1)) by A6, NORMSP_1:28
.= lim ((r (#) f) /* s1) by A3, Th4 ;
hence ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) ) by A3, A7, Th4; :: thesis: verum

end;

hence for b₁ being PartFunc of REAL, the carrier of S st b₁ = r (#) f holds
b₁ is continuous by A1, A2, Th16; :: thesis: verum