for X being RealBanachSpace
for a, b being Real
for y0 being VECTOR of X
for G being Function of X,X st a < b & G is_Lipschitzian_on the carrier of X holds
Fredholm (G,a,b,y0) is with_unique_fixpoint