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

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