theorem Th47: :: ORDEQ_02:21

for X being RealBanachSpace
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