let X be RealBanachSpace; :: thesis: for Z being open Subset of REAL

for a, b being Real

for y0 being VECTOR of X

for y, Gf being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X 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 a, b being Real

for y0 being VECTOR of X

for y, Gf being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X 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 y0 being VECTOR of X

for y, Gf being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X 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 X; :: thesis: for y, Gf being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X 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, the carrier of X; :: thesis: for g being PartFunc of REAL, the carrier of X 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, the carrier of X; :: 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 Th40, Th40a;

reconsider h = y - g as continuous PartFunc of REAL, the carrier of X by A2;

A5: dom h = [.a,b.] /\ [.a,b.] by A1, VFUNCT_1:def 2;

then A7: h is_differentiable_on ].a,b.[ by A1, A2, NDIFF_3:18;

h is_continuous_in x by A5, NFCONT_3:def 2;

then A12: h | ].a,b.[ is constant by A1, Th45, A5, A2, NDIFF_3:18, A8;

A13: for x being Real st x in dom h holds

h /. x = 0. X

y . x = g . x

for a, b being Real

for y0 being VECTOR of X

for y, Gf being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X 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 a, b being Real

for y0 being VECTOR of X

for y, Gf being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X 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 y0 being VECTOR of X

for y, Gf being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X 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 X; :: thesis: for y, Gf being continuous PartFunc of REAL, the carrier of X

for g being PartFunc of REAL, the carrier of X 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, the carrier of X; :: thesis: for g being PartFunc of REAL, the carrier of X 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, the carrier of X; :: 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 Th40, Th40a;

reconsider h = y - g as continuous PartFunc of REAL, the carrier of X by A2;

A5: dom h = [.a,b.] /\ [.a,b.] by A1, VFUNCT_1:def 2;

then A7: h is_differentiable_on ].a,b.[ by A1, A2, NDIFF_3:18;

A8: now :: thesis: for x being Real st x in ].a,b.[ holds

diff (h,x) = 0. X

for x being Real st x in [.a,b.] holds diff (h,x) = 0. X

let x be Real; :: thesis: ( x in ].a,b.[ implies diff (h,x) = 0. X )

assume A9: x in ].a,b.[ ; :: thesis: diff (h,x) = 0. X

then A10: ( diff (y,x) = Gf /. x & diff (g,x) = Gf /. x ) by A1, Th40;

thus diff (h,x) = ((y - g) `| ].a,b.[) . x by A9, A7, NDIFF_3:def 6

.= (Gf /. x) - (Gf /. x) by A10, A1, A2, A5, A9, NDIFF_3:18

.= 0. X by RLVECT_1:15 ; :: thesis: verum

end;assume A9: x in ].a,b.[ ; :: thesis: diff (h,x) = 0. X

then A10: ( diff (y,x) = Gf /. x & diff (g,x) = Gf /. x ) by A1, Th40;

thus diff (h,x) = ((y - g) `| ].a,b.[) . x by A9, A7, NDIFF_3:def 6

.= (Gf /. x) - (Gf /. x) by A10, A1, A2, A5, A9, NDIFF_3:18

.= 0. X by RLVECT_1:15 ; :: thesis: verum

h is_continuous_in x by A5, NFCONT_3:def 2;

then A12: h | ].a,b.[ is constant by A1, Th45, A5, A2, NDIFF_3:18, A8;

A13: for x being Real st x in dom h holds

h /. x = 0. X

proof

for x being Element of REAL st x in dom y holds
let x be Real; :: thesis: ( x in dom h implies h /. x = 0. X )

assume A14: x in dom h ; :: thesis: h /. x = 0. X

A15: a in dom h by A5, A1;

thus h /. x = h /. a by A14, Th46, A12, A5

.= y0 - y0 by A2, A1, A15, VFUNCT_1:def 2

.= 0. X by RLVECT_1:15 ; :: thesis: verum

end;assume A14: x in dom h ; :: thesis: h /. x = 0. X

A15: a in dom h by A5, A1;

thus h /. x = h /. a by A14, Th46, A12, A5

.= y0 - y0 by A2, A1, A15, VFUNCT_1:def 2

.= 0. X by RLVECT_1:15 ; :: thesis: verum

y . x = g . x

proof

hence
y = g
by A1, PARTFUN1:5; :: thesis: verum
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. X = h /. x by A13, A1, A5

.= (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 = y /. x by A16, PARTFUN1:def 6

.= g . x by A17, A16, A1, PARTFUN1:def 6 ; :: thesis: verum

end;assume A16: x in dom y ; :: thesis: y . x = g . x

then 0. X = h /. x by A13, A1, A5

.= (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 = y /. x by A16, PARTFUN1:def 6

.= g . x by A17, A16, A1, PARTFUN1:def 6 ; :: thesis: verum