let x0 be positive Real; :: thesis: for f being Element of the carrier of (Polynom-Ring INT.Ring) holds (exp_R1 (#) ('F' f)) | [.0,x0.] is continuous
let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: (exp_R1 (#) ('F' f)) | [.0,x0.] is continuous
set f1 = exp_R ^ ;
set f2 = 'F' f;
( dom (exp_R ^) = REAL & dom ('F' f) = REAL ) by Lm23, Lm23A;
then A3: dom (('F' f) | [.0,x0.]) = [.0,x0.] by RELAT_1:62;
A2: dom ((exp_R ^) | [.0,x0.]) = [.0,x0.] by Lm23A, RELAT_1:62;
A4: ((exp_R ^) (#) ('F' f)) | [.0,x0.] = ((exp_R ^) | [.0,x0.]) (#) (('F' f) | [.0,x0.]) by RFUNCT_1:45;
for r being Real st r in dom (((exp_R ^) (#) ('F' f)) | [.0,x0.]) holds
((exp_R ^) (#) ('F' f)) | [.0,x0.] is_continuous_in r

proof

let r be Real; :: thesis: ( r in dom (((exp_R ^) (#) ('F' f)) | [.0,x0.]) implies ((exp_R ^) (#) ('F' f)) | [.0,x0.] is_continuous_in r )
assume A5: r in dom (((exp_R ^) (#) ('F' f)) | [.0,x0.]) ; :: thesis: ((exp_R ^) (#) ('F' f)) | [.0,x0.] is_continuous_in r
A6: dom (((exp_R ^) (#) ('F' f)) | [.0,x0.]) = dom (((exp_R ^) | [.0,x0.]) (#) (('F' f) | [.0,x0.])) by RFUNCT_1:45
.= (dom ((exp_R ^) | [.0,x0.])) /\ (dom (('F' f) | [.0,x0.])) by VALUED_1:def 4
.= [.0,x0.] by A2, A3 ;
then A7: (exp_R ^) | [.0,x0.] is_continuous_in r by A2, A5, Lm29, FCONT_1:def 2;
A8: ('F' f) | [.0,x0.] is_continuous_in r by A5, A6, A3, Lm30, FCONT_1:def 2;
r in (dom ((exp_R ^) | [.0,x0.])) /\ (dom (('F' f) | [.0,x0.])) by A2, A3, A5, A6;
hence ((exp_R ^) (#) ('F' f)) | [.0,x0.] is_continuous_in r by A4, A7, A8, FCONT_1:7; :: thesis: verum

end;

hence (exp_R1 (#) ('F' f)) | [.0,x0.] is continuous by FCONT_1:def 2; :: thesis: verum