let x0, r be real number ; :: thesis: for f being PartFunc of REAL ,REAL st x0 in dom f & f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let f be PartFunc of REAL ,REAL ; :: thesis: ( x0 in dom f & f is_continuous_in x0 implies r (#) f is_continuous_in x0 )
assume x0 in dom f ; :: thesis: ( not f is_continuous_in x0 or r (#) f is_continuous_in x0 )
then A1: x0 in dom (r (#) f) by VALUED_1:def 5;
assume A2: f is_continuous_in x0 ; :: thesis: r (#) f is_continuous_in x0
let s1 be Real_Sequence; :: according to FCONT_1:def 1 :: thesis: ( rng s1 c= dom (r (#) f) & s1 is convergent & lim s1 = x0 implies ( (r (#) f) /* s1 is convergent & (r (#) f) . x0 = lim ((r (#) f) /* s1) ) )
assume that
A3: rng s1 c= dom (r (#) f) and
A4: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) . x0 = lim ((r (#) f) /* s1) )
A5: rng s1 c= dom f by A3, VALUED_1:def 5;
then A6: f . x0 = lim (f /* s1) by A2, A4, Def1;
A7: f /* s1 is convergent by A2, A4, A5, Def1;
then r (#) (f /* s1) is convergent by SEQ_2:21;
hence (r (#) f) /* s1 is convergent by A5, RFUNCT_2:24; :: thesis: (r (#) f) . x0 = lim ((r (#) f) /* s1)
thus (r (#) f) . x0 = r * (f . x0) by A1, VALUED_1:def 5
.= lim (r (#) (f /* s1)) by A7, A6, SEQ_2:22
.= lim ((r (#) f) /* s1) by A5, RFUNCT_2:24 ; :: thesis: verum