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

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