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 y, Gf being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & dom y = ['a,b'] & dom g = ['a,b'] & dom Gf = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds
diff (y,t) = Gf /. t ) & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) holds
y = g
let a, b be Real; :: thesis: for Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for y, Gf being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & dom y = ['a,b'] & dom g = ['a,b'] & dom Gf = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds
diff (y,t) = Gf /. t ) & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) holds
y = g
let Z be open Subset of REAL; :: thesis: for y0 being VECTOR of (REAL-NS n)
for y, Gf being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & dom y = ['a,b'] & dom g = ['a,b'] & dom Gf = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds
diff (y,t) = Gf /. t ) & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) holds
y = g
let y0 be VECTOR of (REAL-NS n); :: thesis: for y, Gf being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & dom y = ['a,b'] & dom g = ['a,b'] & dom Gf = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds
diff (y,t) = Gf /. t ) & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) holds
y = g
let y, Gf be continuous PartFunc of REAL,(REAL-NS n); :: thesis: for g being PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & dom y = ['a,b'] & dom g = ['a,b'] & dom Gf = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds
diff (y,t) = Gf /. t ) & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) holds
y = g
let g be PartFunc of REAL,(REAL-NS n); :: thesis: ( a < b & Z = ].a,b.[ & dom y = ['a,b'] & dom g = ['a,b'] & dom Gf = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds
diff (y,t) = Gf /. t ) & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) implies y = g )
assume A1: ( a < b & Z = ].a,b.[ & dom y = ['a,b'] & dom g = ['a,b'] & dom Gf = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds
diff (y,t) = Gf /. t ) & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) ) ; :: thesis: y = g
then A2: ( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = Gf /. t ) ) by Th36;
A3: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
A4: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
reconsider h = y - g as continuous PartFunc of REAL,(REAL-NS n) by A2;
A5: dom h = ['a,b'] /\ ['a,b'] by A1, VFUNCT_1:def 2
.= ['a,b'] ;
then A6: ].a,b.[ c= dom h by A3, XXREAL_1:25;
A7: h is_differentiable_on ].a,b.[ by A1, A2, NDIFF_3:18, A4, A3, A5;

A8: now :: thesis: for x being Real st x in ].a,b.[ holds
diff (h,x) = 0. (REAL-NS n)

let x be Real; :: thesis: ( x in ].a,b.[ implies diff (h,x) = 0. (REAL-NS n) )
assume A9: x in ].a,b.[ ; :: thesis: diff (h,x) = 0. (REAL-NS n)
then A10: diff (y,x) = Gf /. x by A1;
A11: diff (g,x) = Gf /. x by A1, A9, Th36;
thus diff (h,x) = ((y - g) `| ].a,b.[) . x by A9, A7, NDIFF_3:def 6
.= (Gf /. x) - (Gf /. x) by A10, A11, A1, A2, A6, A9, NDIFF_3:18
.= 0. (REAL-NS n) by RLVECT_1:15 ; :: thesis: verum

end;

A12: h | ].a,b.[ is constant by Th41, A5, A7, A8, A3, XXREAL_1:25;
A13: for x being Real st x in dom h holds
h . x = 0. (REAL-NS n)

proof

let x be Real; :: thesis: ( x in dom h implies h . x = 0. (REAL-NS n) )
assume A14: x in dom h ; :: thesis: h . x = 0. (REAL-NS n)
A15: a in dom h by A5, A1, A3;
thus h . x = h . a by A14, Th42, A1, A12, A3, A5
.= h /. a by A15, PARTFUN1:def 6
.= y0 - y0 by A2, A1, A15, VFUNCT_1:def 2
.= 0. (REAL-NS n) by RLVECT_1:15 ; :: thesis: verum

end;

for x being Element of REAL st x in dom y holds
y . x = g . x

proof

let x be Element of REAL ; :: thesis: ( x in dom y implies y . x = g . x )
assume A16: x in dom y ; :: thesis: y . x = g . x
then 0. (REAL-NS n) = h . x by A13, A1, A5
.= h /. x by A16, A1, A5, PARTFUN1:def 6
.= (y /. x) - (g /. x) by A16, A1, A5, VFUNCT_1:def 2 ;
then A17: y /. x = g /. x by RLVECT_1:21;
thus y . x = g /. x by A17, A16, PARTFUN1:def 6
.= g . x by A16, A1, PARTFUN1:def 6 ; :: thesis: verum

end;

hence y = g by A1, PARTFUN1:5; :: thesis: verum