let n be non zero Element of NAT ; :: thesis: 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
Fredholm (G,a,b,y0) is with_unique_fixpoint
let a, b be Real; :: thesis: 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
Fredholm (G,a,b,y0) is with_unique_fixpoint
let y0 be VECTOR of (REAL-NS n); :: thesis: 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
Fredholm (G,a,b,y0) is with_unique_fixpoint
let G be Function of (REAL-NS n),(REAL-NS n); :: thesis: ( a < b & G is_Lipschitzian_on the carrier of (REAL-NS n) implies Fredholm (G,a,b,y0) is with_unique_fixpoint )
assume ( a < b & G is_Lipschitzian_on the carrier of (REAL-NS n) ) ; :: 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 Th52;
hence Fredholm (G,a,b,y0) is with_unique_fixpoint by Th7; :: thesis: verum