let x0 be positive Real; :: thesis: (exp_R ^) | [.0,x0.] is continuous
for r being Real st r in dom ((exp_R ^) | [.0,x0.]) holds
(exp_R ^) | [.0,x0.] is_continuous_in r

proof

let r be Real; :: thesis: ( r in dom ((exp_R ^) | [.0,x0.]) implies (exp_R ^) | [.0,x0.] is_continuous_in r )
assume A1: r in dom ((exp_R ^) | [.0,x0.]) ; :: thesis: (exp_R ^) | [.0,x0.] is_continuous_in r
A2: dom ((exp_R ^) | [.0,x0.]) = [.0,x0.] by Lm23A, RELAT_1:62;
exp_R . r <> 0 by SIN_COS:54;
then exp_R ^ is_continuous_in r by FCONT_1:10, A1, SIN_COS:47, FCONT_1:def 2;
hence (exp_R ^) | [.0,x0.] is_continuous_in r by A1, A2, FCONT_1:1; :: thesis: verum

end;

hence (exp_R ^) | [.0,x0.] is continuous by FCONT_1:def 2; :: thesis: verum