let n be non zero Element of NAT ; :: thesis: for a, b being Real
for Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for f being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) holds
( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
let a, b be Real; :: thesis: for Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for f being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) holds
( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
let Z be open Subset of REAL; :: thesis: for y0 being VECTOR of (REAL-NS n)
for f being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) holds
( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
let y0 be VECTOR of (REAL-NS n); :: thesis: for f being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) holds
( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
let f be continuous PartFunc of REAL,(REAL-NS n); :: thesis: for g being PartFunc of REAL,(REAL-NS n) st a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) holds
( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
let g be PartFunc of REAL,(REAL-NS n); :: thesis: ( a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) implies ( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) ) )
assume A1: ( a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) ) ; :: thesis: ( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
A2: f is_integrable_on ['a,b'] by A1, Th33;
A3: f | ['a,b'] is bounded by A1, Th32;
A4: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
deffunc H₁( Element of REAL ) -> Element of the carrier of (REAL-NS n) = integral (f,a,$1);
consider F0 being Function of REAL,(REAL-NS n) such that
A5: for x being Element of REAL holds F0 . x = H₁(x) from FUNCT_2:sch 4();
set F = F0 | ['a,b'];
A6: dom (F0 | ['a,b']) = (dom F0) /\ ['a,b'] by RELAT_1:61
.= REAL /\ ['a,b'] by FUNCT_2:def 1
.= ['a,b'] by XBOOLE_1:28 ;

A7: now :: thesis: for x being Real st x in [.a,b.] holds
(F0 | ['a,b']) . x = integral (f,a,x)

let x be Real; :: thesis: ( x in [.a,b.] implies (F0 | ['a,b']) . x = integral (f,a,x) )
assume x in [.a,b.] ; :: thesis: (F0 | ['a,b']) . x = integral (f,a,x)
then A8: x in ['a,b'] by A1, INTEGRA5:def 3;
A9: x in REAL by XREAL_0:def 1;
thus (F0 | ['a,b']) . x = F0 . x by A8, A6, FUNCT_1:47
.= integral (f,a,x) by A5, A9 ; :: thesis: verum

end;

A10: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
A11: for x being Real st x in [.a,b.] holds
F0 | ['a,b'] is_continuous_in x by Th34, A1, A6, A7;
A12: for x being Real st x in ].a,b.[ holds
(F0 | ['a,b']) . x = integral (f,a,x) by A7, A10;
A13: Z c= dom (F0 | ['a,b']) by A1, A6, A10, INTEGRA5:def 3;

A14: now :: thesis: for x being Real st x in Z holds
( F0 | ['a,b'] is_differentiable_in x & diff ((F0 | ['a,b']),x) = f /. x )

let x be Real; :: thesis: ( x in Z implies ( F0 | ['a,b'] is_differentiable_in x & diff ((F0 | ['a,b']),x) = f /. x ) )
assume A15: x in Z ; :: thesis: ( F0 | ['a,b'] is_differentiable_in x & diff ((F0 | ['a,b']),x) = f /. x )
then f is_continuous_in x by A10, A4, A1, NFCONT_3:def 2;
hence ( F0 | ['a,b'] is_differentiable_in x & diff ((F0 | ['a,b']),x) = f /. x ) by A15, A1, A2, A3, A12, A13, INTEGR19:55; :: thesis: verum

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 A13, NDIFF_3:10;
set G0 = REAL --> y0;
set G = (REAL --> y0) | ['a,b'];
A17: dom ((REAL --> y0) | ['a,b']) = (dom (REAL --> y0)) /\ ['a,b'] by RELAT_1:61
.= REAL /\ ['a,b']
.= ['a,b'] by XBOOLE_1:28 ;

A18: now :: thesis: for x being Real st x in [.a,b.] holds
((REAL --> y0) | ['a,b']) . x = y0

let x be Real; :: thesis: ( x in [.a,b.] implies ((REAL --> y0) | ['a,b']) . x = y0 )
assume x in [.a,b.] ; :: thesis: ((REAL --> y0) | ['a,b']) . x = y0
then A19: x in ['a,b'] by A1, INTEGRA5:def 3;
thus ((REAL --> y0) | ['a,b']) . x = (REAL --> y0) . x by A19, A17, FUNCT_1:47
.= y0 by XREAL_0:def 1, FUNCOP_1:7 ; :: thesis: verum

end;

A20: F0 | ['a,b'] is continuous by A4, A6, A11, NFCONT_3:def 2;
A21: ((REAL --> y0) | ['a,b']) | Z is constant ;
then A22: ( (REAL --> y0) | ['a,b'] is_differentiable_on Z & ( for x being Real st x in Z holds
(((REAL --> y0) | ['a,b']) `| Z) . x = 0. (REAL-NS n) ) ) by A17, A1, A10, A4, NDIFF_3:20;
A23: dom g = (dom (F0 | ['a,b'])) /\ (dom ((REAL --> y0) | ['a,b'])) by A6, A17, A1;

now :: thesis: for x being Element of REAL st x in dom g holds
g /. x = (((REAL --> y0) | ['a,b']) /. x) + ((F0 | ['a,b']) /. x)

let x be Element of REAL ; :: thesis: ( x in dom g implies g /. x = (((REAL --> y0) | ['a,b']) /. x) + ((F0 | ['a,b']) /. x) )
assume A24: x in dom g ; :: thesis: g /. x = (((REAL --> y0) | ['a,b']) /. x) + ((F0 | ['a,b']) /. x)
A25: x in [.a,b.] by A24, A1, INTEGRA5:def 3;
A26: ((REAL --> y0) | ['a,b']) /. x = ((REAL --> y0) | ['a,b']) . x by A24, A1, A17, PARTFUN1:def 6
.= y0 by A25, A18 ;
A27: (F0 | ['a,b']) /. x = (F0 | ['a,b']) . x by A24, A1, A6, PARTFUN1:def 6
.= integral (f,a,x) by A25, A7 ;
thus g /. x = g . x by A24, PARTFUN1:def 6
.= (((REAL --> y0) | ['a,b']) /. x) + ((F0 | ['a,b']) /. x) by A26, A27, A1, A24 ; :: thesis: verum

end;

then A28: g = ((REAL --> y0) | ['a,b']) + (F0 | ['a,b']) by A23, VFUNCT_1:def 1;
thus g is continuous by A20, A28; :: thesis: ( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
A29: a in ['a,b'] by A1, A4;
A30: 0. (REAL-NS n) = (integral (f,a,a)) - (integral (f,a,a)) by RLVECT_1:15
.= ((integral (f,a,a)) + (integral (f,a,a))) - (integral (f,a,a)) by A29, A1, Th33, A3, INTEGR19:53
.= (integral (f,a,a)) + ((integral (f,a,a)) - (integral (f,a,a))) by RLVECT_1:28
.= (integral (f,a,a)) + (0. (REAL-NS n)) by RLVECT_1:15
.= integral (f,a,a) ;
thus g /. a = g . a by A1, A29, PARTFUN1:def 6
.= y0 + (integral (f,a,a)) by A1, A29
.= y0 by A30 ; :: thesis: ( g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )
A31: ( g is_differentiable_on Z & ( for x being Real st x in Z holds
(g `| Z) . x = (diff (((REAL --> y0) | ['a,b']),x)) + (diff ((F0 | ['a,b']),x)) ) ) by A28, A16, A22, A1, A10, A4, NDIFF_3:17;
thus g is_differentiable_on Z by A28, A16, A22, A1, A10, A4, NDIFF_3:17; :: thesis: for t being Real st t in Z holds
diff (g,t) = f /. t
thus for t being Real st t in Z holds
diff (g,t) = f /. t :: thesis: verum

proof

let t be Real; :: thesis: ( t in Z implies diff (g,t) = f /. t )
assume A32: t in Z ; :: thesis: diff (g,t) = f /. t
A33: diff (g,t) = (g `| Z) . t by A31, A32, NDIFF_3:def 6
.= (diff (((REAL --> y0) | ['a,b']),t)) + (diff ((F0 | ['a,b']),t)) by A28, A16, A22, A1, A10, A4, NDIFF_3:17, A32 ;
A34: diff (((REAL --> y0) | ['a,b']),t) = (((REAL --> y0) | ['a,b']) `| Z) . t by A22, A32, NDIFF_3:def 6
.= 0. (REAL-NS n) by A21, A17, A1, A10, A4, NDIFF_3:20, A32 ;
thus diff (g,t) = (0. (REAL-NS n)) + (f /. t) by A33, A34, A14, A32
.= f /. t ; :: thesis: verum

end;