let a, b be Real; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
assume A1: ( a <= b & ['a,b'] c= dom f & f is continuous ) ; :: thesis:
then f | ['a,b'] is continuous ;
then A2: ( f | ['a,b'] is bounded & f is_integrable_on ['a,b'] ) by A1, INTEGRA5:10, INTEGRA5:11;
deffunc H₁( Real) -> Element of REAL = In ((integral (f,a,$1)),REAL);
consider F0 being Function of REAL,REAL such that
A3: for t being Element of REAL holds F0 . t = H₁(t) from FUNCT_2:sch 4();
A4: for t being Real holds F0 . t = integral (f,a,t)

let t be Real; :: thesis:
t in REAL by XREAL_0:def 1;
then F0 . t = In ((integral (f,a,t)),REAL) by A3;
hence F0 . t = integral (f,a,t) ; :: thesis:

end;

set F = F0 | [.a,b.];
dom F0 = REAL by FUNCT_2:def 1;
then A5: dom (F0 | [.a,b.]) = [.a,b.] by RELAT_1:62;
reconsider F = F0 | [.a,b.] as PartFunc of REAL,REAL ;
take F ; :: thesis:
thus A6: ].a,b.[ c= dom F by A5, XXREAL_1:25; :: thesis:
thus A7: for t being Real st t in ].a,b.[ holds
F . t = integral (f,a,t) :: thesis:

let t be Real; :: thesis:
assume A8: t in ].a,b.[ ; :: thesis:
].a,b.[ c= [.a,b.] by XXREAL_1:25;
hence F . t = F0 . t by FUNCT_1:49, A8
.= integral (f,a,t) by A4 ;
:: thesis:

end;

let t be Real; :: thesis:
assume A9: t in ].a,b.[ ; :: thesis:
].a,b.[ c= [.a,b.] by XXREAL_1:25;
then t in [.a,b.] by A9;
then t in ['a,b'] by A1, INTEGRA5:def 3;
then f is_continuous_in t by A1;
hence ( F is_differentiable_in t & diff (F,t) = f . t ) by A1, A2, A7, A6, A9, INTEGRA6:28; :: thesis: