let X be RealBanachSpace; :: thesis:
let Z be open Subset of REAL; :: thesis:
let a, b be Real; :: thesis:
let y0 be VECTOR of X; :: thesis:
let f be continuous PartFunc of REAL, the carrier of X; :: thesis:
let g be PartFunc of REAL, the carrier of X; :: thesis:
assume that
A2: dom f = [.a,b.] and
A3: dom g = [.a,b.] and
D1: Z = ].a,b.[ and
D2: for t being Real st t in [.a,b.] holds
g /. t = y0 + (integral (f,a,t)) ; :: thesis:
deffunc H₁( Element of REAL ) -> Element of the carrier of X = integral (f,a,$1);
consider F0 being Function of REAL, the carrier of X such that
A5: for x being Element of REAL holds F0 . x = H₁(x) from FUNCT_2:sch 4();
set G0 = REAL --> y0;
set F = F0 | [.a,b.];
set G = (REAL --> y0) | [.a,b.];
( dom (F0 | [.a,b.]) = (dom F0) /\ [.a,b.] & dom ((REAL --> y0) | [.a,b.]) = (dom (REAL --> y0)) /\ [.a,b.] ) by RELAT_1:61;
then ( dom (F0 | [.a,b.]) = REAL /\ [.a,b.] & dom ((REAL --> y0) | [.a,b.]) = REAL /\ [.a,b.] ) by FUNCT_2:def 1;
then A6: ( dom (F0 | [.a,b.]) = [.a,b.] & dom ((REAL --> y0) | [.a,b.]) = [.a,b.] & dom g = (dom (F0 | [.a,b.])) /\ (dom ((REAL --> y0) | [.a,b.])) ) by A3, XBOOLE_1:28;
A10: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
A7: for x being Real st x in [.a,b.] holds
(F0 | [.a,b.]) /. x = integral (f,a,x)

proof

let x be Real; :: thesis:
assume x in [.a,b.] ; :: thesis:
then A8: ( (F0 | [.a,b.]) /. x = (F0 | [.a,b.]) . x & (F0 | [.a,b.]) . x = F0 . x ) by A6, PARTFUN1:def 6, FUNCT_1:47;
x in REAL by XREAL_0:def 1;
hence (F0 | [.a,b.]) /. x = integral (f,a,x) by A5, A8; :: thesis:

end;

then A12: for x being Real st x in ].a,b.[ holds
(F0 | [.a,b.]) /. x = integral (f,a,x) by A10;

A14: now :: thesis:

let x be Real; :: thesis:
assume A15: x in Z ; :: thesis:
then f is_continuous_in x by A10, A2, D1, NFCONT_3:def 2;
hence ( F0 | [.a,b.] is_differentiable_in x & diff ((F0 | [.a,b.]),x) = f /. x ) by A15, A2, D1, A12, A10, A6, Th1955; :: thesis:

end;

then for x being Real st x in Z holds
F0 | [.a,b.] is_differentiable_in x ;
then A16: F0 | [.a,b.] is_differentiable_on Z by D1, A6, XXREAL_1:25, NDIFF_3:10;

A18: now :: thesis:

let x be Real; :: thesis:
assume A19: x in [.a,b.] ; :: thesis:
then ((REAL --> y0) | [.a,b.]) /. x = ((REAL --> y0) | [.a,b.]) . x by A6, PARTFUN1:def 6;
then ((REAL --> y0) | [.a,b.]) /. x = (REAL --> y0) . x by A19, A6, FUNCT_1:47;
hence ((REAL --> y0) | [.a,b.]) /. x = y0 by XREAL_0:def 1, FUNCOP_1:7; :: thesis:

end;

((REAL --> y0) | [.a,b.]) | Z is constant ;
then A23: ( (REAL --> y0) | [.a,b.] is_differentiable_on Z & ( for x being Real st x in Z holds
(((REAL --> y0) | [.a,b.]) `| Z) . x = 0. X ) ) by A6, D1, A10, NDIFF_3:20;

now :: thesis:

let x be Element of REAL ; :: thesis:
assume A25: x in dom g ; :: thesis:
then ( ((REAL --> y0) | [.a,b.]) /. x = y0 & (F0 | [.a,b.]) /. x = integral (f,a,x) ) by A3, A7, A18;
hence g /. x = (((REAL --> y0) | [.a,b.]) /. x) + ((F0 | [.a,b.]) /. x) by A3, D2, A25; :: thesis:

end;

then A29: g = ((REAL --> y0) | [.a,b.]) + (F0 | [.a,b.]) by A6, VFUNCT_1:def 1;
F0 | [.a,b.] is continuous by A6, A7, Th35, A2;
hence g is continuous by A29; :: thesis:
thus B1: g is_differentiable_on Z by A29, A16, A23, A3, D1, A10, NDIFF_3:17; :: thesis:
thus for t being Real st t in Z holds
diff (g,t) = f /. t :: thesis:

proof

let t be Real; :: thesis:
assume A33: t in Z ; :: thesis:
then ( diff (g,t) = (g `| Z) . t & (g `| Z) . t = (diff (((REAL --> y0) | [.a,b.]),t)) + (diff ((F0 | [.a,b.]),t)) & diff (((REAL --> y0) | [.a,b.]),t) = (((REAL --> y0) | [.a,b.]) `| Z) . t & (((REAL --> y0) | [.a,b.]) `| Z) . t = 0. X ) by A23, B1, A29, A16, NDIFF_3:17, NDIFF_3:def 6;
hence diff (g,t) = f /. t by A14, A33; :: thesis:

end;