set X = dom f;

A1: dom f c= dom (r (#) f) by VALUED_1:def 5;

A2: f | (dom f) is continuous ;

then (r (#) f) | (dom f) = r (#) f ;

hence for b_{1} being PartFunc of REAL,REAL st b_{1} = r (#) f holds

b_{1} is continuous
by A1, A3, Th13; :: thesis: verum

A1: dom f c= dom (r (#) f) by VALUED_1:def 5;

A2: f | (dom f) is continuous ;

A3: 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) )

dom (r (#) f) = dom f
by VALUED_1:def 5;( (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

A4: rng s1 c= dom f and

A5: s1 is convergent and

A6: lim s1 in dom f ; :: thesis: ( (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; :: thesis: verum

end;assume that

A4: rng s1 c= dom f and

A5: s1 is convergent and

A6: lim s1 in dom f ; :: thesis: ( (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; :: thesis: verum

then (r (#) f) | (dom f) = r (#) f ;

hence for b

b