theorem Th58: :: ORDEQ_02:27

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
for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (Fredholm (G,a,b,y0)) . f holds
( g /. a = y0 & g is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = (G * f) /. t ) )