theorem Th36: :: ORDEQ_01:36

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 f being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (f,a,t)) ) holds
( g is continuous & g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )