let x0 be positive Real; :: thesis: for f being Element of the carrier of (Polynom-Ring INT.Ring) holds ('F' f) | [.0,x0.] is continuous
let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: ('F' f) | [.0,x0.] is continuous
set F = 'F' f;
A1: dom ('F' f) = REAL by Lm23;
for r being Real st r in dom (('F' f) | [.0,x0.]) holds
('F' f) | [.0,x0.] is_continuous_in r

proof

let r be Real; :: thesis: ( r in dom (('F' f) | [.0,x0.]) implies ('F' f) | [.0,x0.] is_continuous_in r )
assume A2: r in dom (('F' f) | [.0,x0.]) ; :: thesis: ('F' f) | [.0,x0.] is_continuous_in r
dom (('F' f) | [.0,x0.]) = [.0,x0.] by A1, RELAT_1:62;
hence ('F' f) | [.0,x0.] is_continuous_in r by A1, FCONT_1:def 2, FCONT_1:1, A2; :: thesis: verum

end;

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