let n be non zero Element of NAT ; :: thesis: for a, b being Real
for Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n)
for y1, y2 being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n)
for y1, y2 being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n)
for y1, y2 being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 (REAL-NS n); :: thesis: for G being Function of (REAL-NS n),(REAL-NS n)
for y1, y2 being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 (REAL-NS n),(REAL-NS n); :: thesis: for y1, y2 being continuous PartFunc of REAL,(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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,(REAL-NS n); :: thesis: ( a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) & 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 (REAL-NS n) & 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 Th53;
then consider y being set such that
A2: ( 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 ) ) ;
A3: y1 is_a_fixpoint_of Fredholm (G,a,b,y0) by Th55, A1;
A4: y2 is_a_fixpoint_of Fredholm (G,a,b,y0) by Th55, A1;
y1 = y by A3, A2
.= y2 by A4, A2 ;
hence y1 = y2 ; :: thesis: verum