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;
for x being Real st x in [.a,b.] holds
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 for x being Element of REAL st x in dom y holds
y . x = g . x hence y = g by A1, PARTFUN1:5; :: thesis: verum