theorem Th43: :: ORDEQ_01:43

for n being non zero Element of NAT
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