theorem Th54: :: ORDEQ_01:54

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 G being Function of (REAL-NS n),(REAL-NS n)
for f, g being continuous PartFunc of REAL,(REAL-NS n) st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 ) )