let X be RealBanachSpace; :: thesis: for Z being open Subset of REAL
for a, b being Real
for y0 being VECTOR of X
for G being Function of X,X
for y1, y2 being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & dom y1 = ['a,b'] & y1 is_differentiable_on Z & y1 /. a = y0 & ( for t being Real st t in Z holds
diff (y1,t) = G . (y1 /. t) ) & dom y2 = ['a,b'] & y2 is_differentiable_on Z & y2 /. a = y0 & ( for t being Real st t in Z holds
diff (y2,t) = G . (y2 /. t) ) holds
y1 = y2
let Z be open Subset of REAL; :: thesis: for a, b being Real
for y0 being VECTOR of X
for G being Function of X,X
for y1, y2 being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & dom y1 = ['a,b'] & y1 is_differentiable_on Z & y1 /. a = y0 & ( for t being Real st t in Z holds
diff (y1,t) = G . (y1 /. t) ) & dom y2 = ['a,b'] & y2 is_differentiable_on Z & y2 /. a = y0 & ( for t being Real st t in Z holds
diff (y2,t) = G . (y2 /. t) ) holds
y1 = y2
let a, b be Real; :: thesis: for y0 being VECTOR of X
for G being Function of X,X
for y1, y2 being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & dom y1 = ['a,b'] & y1 is_differentiable_on Z & y1 /. a = y0 & ( for t being Real st t in Z holds
diff (y1,t) = G . (y1 /. t) ) & dom y2 = ['a,b'] & y2 is_differentiable_on Z & y2 /. a = y0 & ( for t being Real st t in Z holds
diff (y2,t) = G . (y2 /. t) ) holds
y1 = y2
let y0 be VECTOR of X; :: thesis: for G being Function of X,X
for y1, y2 being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & dom y1 = ['a,b'] & y1 is_differentiable_on Z & y1 /. a = y0 & ( for t being Real st t in Z holds
diff (y1,t) = G . (y1 /. t) ) & dom y2 = ['a,b'] & y2 is_differentiable_on Z & y2 /. a = y0 & ( for t being Real st t in Z holds
diff (y2,t) = G . (y2 /. t) ) holds
y1 = y2
let G be Function of X,X; :: thesis: for y1, y2 being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & dom y1 = ['a,b'] & y1 is_differentiable_on Z & y1 /. a = y0 & ( for t being Real st t in Z holds
diff (y1,t) = G . (y1 /. t) ) & dom y2 = ['a,b'] & y2 is_differentiable_on Z & y2 /. a = y0 & ( for t being Real st t in Z holds
diff (y2,t) = G . (y2 /. t) ) holds
y1 = y2
let y1, y2 be continuous PartFunc of REAL, the carrier of X; :: thesis: ( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & dom y1 = ['a,b'] & y1 is_differentiable_on Z & y1 /. a = y0 & ( for t being Real st t in Z holds
diff (y1,t) = G . (y1 /. t) ) & dom y2 = ['a,b'] & y2 is_differentiable_on Z & y2 /. a = y0 & ( for t being Real st t in Z holds
diff (y2,t) = G . (y2 /. t) ) implies y1 = y2 )
assume A1: ( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & dom y1 = ['a,b'] & y1 is_differentiable_on Z & y1 /. a = y0 & ( for t being Real st t in Z holds
diff (y1,t) = G . (y1 /. t) ) & dom y2 = ['a,b'] & y2 is_differentiable_on Z & y2 /. a = y0 & ( for t being Real st t in Z holds
diff (y2,t) = G . (y2 /. t) ) ) ; :: thesis: y1 = y2
then Fredholm (G,a,b,y0) is with_unique_fixpoint by Th57;
then consider y being set such that
SS: ( y is_a_fixpoint_of Fredholm (G,a,b,y0) & ( for z being set st z is_a_fixpoint_of Fredholm (G,a,b,y0) holds
y = z ) ) ;
y1 = y by Th59, A1, SS
.= y2 by Th59, A1, SS ;
hence y1 = y2 ; :: thesis: verum