for n being non zero Element of NAT
for a, b being Real
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n) st a < b & G is_Lipschitzian_on the carrier of (REAL-NS n) holds
ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction