let X be RealBanachSpace; :: thesis: 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
let a, b be Real; :: thesis: 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
let y0 be VECTOR of X; :: thesis: 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
let G be Function of X,X; :: thesis: ( a < b & G is_Lipschitzian_on the carrier of X implies Fredholm (G,a,b,y0) is with_unique_fixpoint )
assume ( a < b & G is_Lipschitzian_on the carrier of X ) ; :: thesis: Fredholm (G,a,b,y0) is with_unique_fixpoint
then ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction by Th56;
hence Fredholm (G,a,b,y0) is with_unique_fixpoint by ORDEQ_01:7; :: thesis: verum