theorem Th40a: :: ORDEQ_02:16

for X being RealBanachSpace
for a, b being Real
for y0 being VECTOR of X
for f being continuous PartFunc of REAL, the carrier of X
for g being PartFunc of REAL, the carrier of X st a <= b & dom f = [.a,b.] & ( for t being Real st t in [.a,b.] holds
g /. t = y0 + (integral (f,a,t)) ) holds
g /. a = y0