theorem :: ORDEQ_02:30

for X being RealBanachSpace
for Z being open Subset of REAL
for a, b being Real
for y0 being VECTOR of X
for G being Function of X,X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X holds
ex y being continuous PartFunc of REAL, the carrier of X st
( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds
diff (y,t) = G . (y /. t) ) )