theorem Th55: :: ORDEQ_01:55

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 y being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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) ) holds
y is_a_fixpoint_of Fredholm (G,a,b,y0)