let E, G be RealNormSpace; :: thesis:
let F be RealBanachSpace; :: thesis:
let Z be Subset of [:E,F:]; :: thesis:
let f be PartFunc of [:E,F:],G; :: thesis:
let a be Point of E; :: thesis:
let b be Point of F; :: thesis:
let c be Point of G; :: thesis:
let z be Point of [:E,F:]; :: thesis:
assume that
A1: Z is open and
A2: dom f = Z and
A3: f is_continuous_on Z and
A4: f is_partial_differentiable_on`2 Z and
A5: f `partial`2| Z is_continuous_on Z and
A6: ( z = [a,b] & z in Z ) and
A7: f . (a,b) = c and
A8: partdiff`2 (f,z) is one-to-one and
A9: (partdiff`2 (f,z)) " is Lipschitzian LinearOperator of G,F ; :: thesis:
consider QQ being Lipschitzian LinearOperator of G,F such that
A10: QQ = (partdiff`2 (f,z)) " by A9;
reconsider Q = QQ as Point of (R_NormSpace_of_BoundedLinearOperators (G,F)) by LOPBAN_1:def 9;
set BLQ = ||.Q.||;
reconsider z1 = [a,(0. F)] as Point of [:E,F:] ;
reconsider e0b = [(0. E),b] as Point of [:E,F:] ;
A11: - e0b = [(- (0. E)),(- b)] by PRVECT_3:18
.= [(0. E),(- b)] by RLVECT_1:12 ;
deffunc H₁( Point of [:E,F:]) -> Element of the carrier of [:E,F:] = (1 * $1) + (- e0b);
consider H being Function of the carrier of [:E,F:], the carrier of [:E,F:] such that
A12: for p being Point of [:E,F:] holds H . p = H₁(p) from FUNCT_2:sch 4();
A13: for x being Point of E
for y being Point of F holds H . (x,y) = [x,(y - b)]

let x be Point of E; :: thesis:
let y be Point of F; :: thesis:
reconsider p = [x,y] as Point of [:E,F:] ;
A14: 1 * p = [(1 * x),(1 * y)] by PRVECT_3:18
.= [x,(1 * y)] by RLVECT_1:def 8
.= [x,y] by RLVECT_1:def 8 ;
thus H . (x,y) = (1 * p) + (- e0b) by A12
.= [(x + (0. E)),(y + (- b))] by A11, A14, PRVECT_3:18
.= [x,(y - b)] by RLVECT_1:def 4 ; :: thesis:

end;

A15: dom H = the carrier of [:E,F:] by FUNCT_2:def 1;
deffunc H₂( Point of [:E,F:]) -> Element of the carrier of [:E,F:] = (1 * $1) + e0b;
consider K being Function of the carrier of [:E,F:], the carrier of [:E,F:] such that
A16: for p being Point of [:E,F:] holds K . p = H₂(p) from FUNCT_2:sch 4();
A17: dom K = the carrier of [:E,F:] by FUNCT_2:def 1;
for p being Point of [:E,F:] holds (K * H) . p = p

proof

let p be Point of [:E,F:]; :: thesis:
H . p = (1 * p) + (- e0b) by A12
.= p - e0b by RLVECT_1:def 8 ;
then K . (H . p) = (1 * (p - e0b)) + e0b by A16
.= (p - e0b) + e0b by RLVECT_1:def 8
.= p - (e0b - e0b) by RLVECT_1:29
.= p - (0. [:E,F:]) by RLVECT_1:15
.= p by RLVECT_1:13 ;
hence (K * H) . p = p by A15, FUNCT_1:13; :: thesis:

end;

then A18: K * H = id the carrier of [:E,F:] by FUNCT_2:124;
then A19: ( H is one-to-one & K is onto ) by FUNCT_2:23;
for p being Point of [:E,F:] holds (H * K) . p = p

proof

let p be Point of [:E,F:]; :: thesis:
K . p = (1 * p) + e0b by A16
.= p + e0b by RLVECT_1:def 8 ;
then H . (K . p) = (1 * (p + e0b)) - e0b by A12
.= (p + e0b) - e0b by RLVECT_1:def 8
.= p + (e0b - e0b) by RLVECT_1:28
.= p + (0. [:E,F:]) by RLVECT_1:15
.= p by RLVECT_1:def 4 ;
hence (H * K) . p = p by A17, FUNCT_1:13; :: thesis:

end;

then H * K = id the carrier of [:E,F:] by FUNCT_2:124;
then ( K is one-to-one & H is onto ) by FUNCT_2:23;
then rng H = the carrier of [:E,F:] by FUNCT_2:def 3;
then A20: K = H " by A18, FUNCT_2:23, FUNCT_2:30;
reconsider Z1 = H .: Z as Subset of [:E,F:] ;
A21: for x being Point of E
for y being Point of F holds
( [x,(y + b)] in Z iff [x,y] in Z1 )

proof

let x be Point of E; :: thesis:
let y be Point of F; :: thesis:

hereby :: thesis:

assume A22: [x,(y + b)] in Z ; :: thesis:
reconsider q = [x,(y + b)] as Point of [:E,F:] ;
q in the carrier of [:E,F:] ;
then A23: [x,(y + b)] in dom H by FUNCT_2:def 1;
H . [x,(y + b)] = H . (x,(y + b))
.= [x,((y + b) - b)] by A13
.= [x,(y + (b - b))] by RLVECT_1:28
.= [x,(y + (0. F))] by RLVECT_1:15
.= [x,y] by RLVECT_1:def 4 ;
hence [x,y] in Z1 by A22, A23, FUNCT_1:def 6; :: thesis:

end;

assume [x,y] in Z1 ; :: thesis:
then consider s being object such that
A24: ( s in dom H & s in Z & [x,y] = H . s ) by FUNCT_1:def 6;
consider x1 being Point of E, y1 being Point of F such that
A25: s = [x1,y1] by A24, PRVECT_3:18;
A26: H . [x1,y1] = H . (x1,y1)
.= [x1,(y1 - b)] by A13 ;
then ( x = x1 & y = y1 - b ) by A24, A25, XTUPLE_0:1;
then y + b = y1 - (b - b) by RLVECT_1:29
.= y1 - (0. F) by RLVECT_1:5
.= y1 by RLVECT_1:13 ;
hence [x,(y + b)] in Z by A24, A25, A26, XTUPLE_0:1; :: thesis:

end;

reconsider e0b = [(0. E),b] as Point of [:E,F:] ;
A27: for p being object holds
( p in Z1 iff p in { (y - e0b) where y is Point of [:E,F:] : y in Z } )

proof

let p be object ; :: thesis:
A28: - e0b = [(- (0. E)),(- b)] by PRVECT_3:18
.= [(0. E),(- b)] by RLVECT_1:12 ;

hereby :: thesis:

assume A29: p in Z1 ; :: thesis:
then consider s being Point of E, t being Point of F such that
A30: p = [s,t] by PRVECT_3:18;
A31: [s,(t + b)] in Z by A21, A29, A30;
reconsider y = [s,(t + b)] as Point of [:E,F:] ;
y - e0b = [(s + (0. E)),((t + b) + (- b))] by A28, PRVECT_3:18
.= [s,((t + b) - b)] by RLVECT_1:def 4
.= [s,(t + (b - b))] by RLVECT_1:28
.= [s,(t + (0. F))] by RLVECT_1:15
.= p by A30, RLVECT_1:def 4 ;
hence p in { (y - e0b) where y is Point of [:E,F:] : y in Z } by A31; :: thesis:

end;

assume p in { (y - e0b) where y is Point of [:E,F:] : y in Z } ; :: thesis:
then consider y being Point of [:E,F:] such that
A32: ( p = y - e0b & y in Z ) ;
consider s being Point of E, t being Point of F such that
A33: y = [s,t] by PRVECT_3:18;
A34: p = [(s + (0. E)),(t + (- b))] by A28, A32, A33, PRVECT_3:18
.= [s,(t - b)] by RLVECT_1:def 4 ;
(t - b) + b = t - (b - b) by RLVECT_1:29
.= t - (0. F) by RLVECT_1:15
.= t by RLVECT_1:13 ;
hence p in Z1 by A21, A32, A33, A34; :: thesis:

end;

then A35: Z1 = { (y - e0b) where y is Point of [:E,F:] : y in Z } by TARSKI:2;
A36: Z1 is open by A1, A27, OP2, TARSKI:2;
defpred S₁[ object , object ] means ex x being Point of E ex y being Point of F st
( $1 = [x,y] & $2 = (f /. [x,(y + b)]) - c );
A37: for p being object st p in Z1 holds
ex w being object st
( w in the carrier of G & S₁[p,w] )

proof

let p be object ; :: thesis:
assume p in Z1 ; :: thesis:
then consider x being Point of E, y being Point of F such that
A38: p = [x,y] by PRVECT_3:18;
(f /. [x,(y + b)]) - c is Point of G ;
hence ex w being object st
( w in the carrier of G & S₁[p,w] ) by A38; :: thesis:

end;

consider f1 being Function of Z1,G such that
A39: for p being object st p in Z1 holds
S₁[p,f1 . p] from FUNCT_2:sch 1(A37);
A40: rng f1 c= the carrier of G ;
A41: dom f1 = Z1 by FUNCT_2:def 1;
then f1 in PFuncs ( the carrier of [:E,F:], the carrier of G) by A40, PARTFUN1:def 3;
then reconsider f1 = f1 as PartFunc of [:E,F:],G by PARTFUN1:46;
A42: for x being Point of E
for y being Point of F st [x,y] in Z1 holds
f1 . (x,y) = (f /. [x,(y + b)]) - c

proof

let x be Point of E; :: thesis:
let y be Point of F; :: thesis:
assume [x,y] in Z1 ; :: thesis:
then consider x0 being Point of E, y0 being Point of F such that
A43: ( [x,y] = [x0,y0] & f1 . [x,y] = (f /. [x0,(y0 + b)]) - c ) by A39;
( x = x0 & y = y0 ) by A43, XTUPLE_0:1;
hence f1 . (x,y) = (f /. [x,(y + b)]) - c by A43; :: thesis:

end;

defpred S₂[ object , object ] means ex x being Point of E ex y being Point of F st
( $1 = [x,y] & $2 = Q . (f1 . (x,y)) );
A44: for p being object st p in Z1 holds
ex w being object st
( w in the carrier of F & S₂[p,w] )

proof

let p be object ; :: thesis:
assume A45: p in Z1 ; :: thesis:
then consider x being Point of E, y being Point of F such that
A46: p = [x,y] by PRVECT_3:18;
A47: Q . (f1 /. [x,y]) is Point of F ;
[x,y] in dom f1 by A45, A46, FUNCT_2:def 1;
then f1 /. [x,y] = f1 . (x,y) by PARTFUN1:def 6;
hence ex w being object st
( w in the carrier of F & S₂[p,w] ) by A46, A47; :: thesis:

end;

consider f2 being Function of Z1,F such that
A48: for p being object st p in Z1 holds
S₂[p,f2 . p] from FUNCT_2:sch 1(A44);
A49: rng f2 c= the carrier of F ;
A50: dom f2 = Z1 by FUNCT_2:def 1;
then f2 in PFuncs ( the carrier of [:E,F:], the carrier of F) by A49, PARTFUN1:def 3;
then reconsider f2 = f2 as PartFunc of [:E,F:],F by PARTFUN1:46;
A51: for x being Point of E
for y being Point of F st [x,y] in Z1 holds
f2 . (x,y) = Q . (f1 . (x,y))

proof

let x be Point of E; :: thesis:
let y be Point of F; :: thesis:
assume [x,y] in Z1 ; :: thesis:
then consider x0 being Point of E, y0 being Point of F such that
A52: ( [x,y] = [x0,y0] & f2 . [x,y] = Q . (f1 . (x0,y0)) ) by A48;
thus f2 . (x,y) = Q . (f1 . (x,y)) by A52; :: thesis:

end;

defpred S₃[ object , object ] means ex x being Point of E ex y being Point of F st
( $1 = [x,y] & $2 = y - (f2 /. [x,y]) );
A53: for p being object st p in Z1 holds
ex w being object st
( w in the carrier of F & S₃[p,w] )

proof

let p be object ; :: thesis:
assume p in Z1 ; :: thesis:
then consider x being Point of E, y being Point of F such that
A54: p = [x,y] by PRVECT_3:18;
y - (f2 /. [x,y]) is Point of F ;
hence ex w being object st
( w in the carrier of F & S₃[p,w] ) by A54; :: thesis:

end;

consider Fai being Function of Z1,F such that
A55: for p being object st p in Z1 holds
S₃[p,Fai . p] from FUNCT_2:sch 1(A53);
A56: rng Fai c= the carrier of F ;
A57: dom Fai = Z1 by FUNCT_2:def 1;
then Fai in PFuncs ( the carrier of [:E,F:], the carrier of F) by A56, PARTFUN1:def 3;
then reconsider Fai = Fai as PartFunc of [:E,F:],F by PARTFUN1:46;
A58: for x being Point of E
for y being Point of F st [x,y] in Z1 holds
Fai . (x,y) = y - (f2 /. [x,y])

proof

let x be Point of E; :: thesis:
let y be Point of F; :: thesis:
assume [x,y] in Z1 ; :: thesis:
then consider x0 being Point of E, y0 being Point of F such that
A59: ( [x,y] = [x0,y0] & Fai . [x,y] = y0 - (f2 /. [x0,y0]) ) by A55;
thus Fai . (x,y) = y - (f2 /. [x,y]) by A59, XTUPLE_0:1; :: thesis:

end;

A60: for z0 being Point of [:E,F:]
for r being Real st z0 in Z1 & 0 < r holds
ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.((Fai /. z1) - (Fai /. z0)).|| < r ) )

proof

let z0 be Point of [:E,F:]; :: thesis:
let r be Real; :: thesis:
assume A61: ( z0 in Z1 & 0 < r ) ; :: thesis:
reconsider w0 = z0 + e0b as Point of [:E,F:] ;
consider x0 being Point of E, y0 being Point of F such that
A62: z0 = [x0,y0] by PRVECT_3:18;
A63: 0 < 2 * (||.Q.|| + 1) by XREAL_1:129;
consider ww0 being Point of [:E,F:] such that
A64: ( z0 = ww0 - e0b & ww0 in Z ) by A35, A61;
w0 = ww0 - (e0b - e0b) by A64, RLVECT_1:29
.= ww0 - (0. [:E,F:]) by RLVECT_1:15
.= ww0 by RLVECT_1:13 ;
then consider s being Real such that
A65: ( 0 < s & ( for w1 being Point of [:E,F:] st w1 in Z & ||.(w1 - w0).|| < s holds
||.((f /. w1) - (f /. w0)).|| < r / (2 * (||.Q.|| + 1)) ) ) by A3, A61, A63, A64, NFCONT_1:19, XREAL_1:139;
reconsider s1 = min (s,(r / 2)) as Real ;
A66: 0 < r / 2 by A61, XREAL_1:215;
A67: ( s1 <= s & s1 <= r / 2 ) by XXREAL_0:17;
take s1 ; :: thesis:
thus 0 < s1 by A65, A66, XXREAL_0:15; :: thesis:
thus for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s1 holds
||.((Fai /. z1) - (Fai /. z0)).|| < r :: thesis:

proof

let z1 be Point of [:E,F:]; :: thesis:
assume A68: ( z1 in Z1 & ||.(z1 - z0).|| < s1 ) ; :: thesis:
reconsider w1 = z1 + e0b as Point of [:E,F:] ;
consider x1 being Point of E, y1 being Point of F such that
A69: z1 = [x1,y1] by PRVECT_3:18;
consider ww1 being Point of [:E,F:] such that
A70: ( z1 = ww1 - e0b & ww1 in Z ) by A35, A68;
A71: w1 = ww1 - (e0b - e0b) by A70, RLVECT_1:29
.= ww1 - (0. [:E,F:]) by RLVECT_1:15
.= ww1 by RLVECT_1:13 ;
w1 - w0 = ((z1 + e0b) - e0b) - z0 by RLVECT_1:27
.= z1 - z0 by RLVECT_4:1 ;
then A72: ||.(w1 - w0).|| < s by A67, A68, XXREAL_0:2;
A73: Fai /. z1 = Fai . (x1,y1) by A57, A68, A69, PARTFUN1:def 6
.= y1 - (f2 /. [x1,y1]) by A58, A68, A69 ;
Fai /. z0 = Fai . (x0,y0) by A57, A61, A62, PARTFUN1:def 6
.= y0 - (f2 /. [x0,y0]) by A58, A61, A62 ;
then (Fai /. z1) - (Fai /. z0) = ((y1 - (f2 /. [x1,y1])) - y0) + (f2 /. [x0,y0]) by A73, RLVECT_1:29
.= (y1 - ((f2 /. [x1,y1]) + y0)) + (f2 /. [x0,y0]) by RLVECT_1:27
.= ((y1 - y0) - (f2 /. [x1,y1])) + (f2 /. [x0,y0]) by RLVECT_1:27
.= (y1 - y0) - ((f2 /. [x1,y1]) - (f2 /. [x0,y0])) by RLVECT_1:29 ;
then A75: ||.((Fai /. z1) - (Fai /. z0)).|| <= ||.(y1 - y0).|| + ||.((f2 /. [x1,y1]) - (f2 /. [x0,y0])).|| by NORMSP_1:3;
A76: f2 /. [x1,y1] = f2 . (x1,y1) by A50, A68, A69, PARTFUN1:def 6
.= Q . (f1 . (x1,y1)) by A51, A68, A69 ;
A77: f2 /. [x0,y0] = f2 . (x0,y0) by A50, A61, A62, PARTFUN1:def 6
.= Q . (f1 . (x0,y0)) by A51, A61, A62 ;
[x1,(y1 + b)] = [(x1 + (0. E)),(y1 + b)] by RLVECT_1:4
.= w1 by A69, PRVECT_3:18 ;
then A79: f1 . (x1,y1) = (f /. w1) - c by A42, A68, A69;
[x0,(y0 + b)] = [(x0 + (0. E)),(y0 + b)] by RLVECT_1:4
.= w0 by A62, PRVECT_3:18 ;
then A81: f1 . (x0,y0) = (f /. w0) - c by A42, A61, A62;
A82: ((f /. w1) - c) - ((f /. w0) - c) = (((f /. w1) - c) - (f /. w0)) + c by RLVECT_1:29
.= ((f /. w1) - (c + (f /. w0))) + c by RLVECT_1:27
.= (((f /. w1) - (f /. w0)) - c) + c by RLVECT_1:27
.= ((f /. w1) - (f /. w0)) - (c - c) by RLVECT_1:29
.= ((f /. w1) - (f /. w0)) - (0. G) by RLVECT_1:15
.= (f /. w1) - (f /. w0) by RLVECT_1:13 ;
A83: QQ is additive ;
A84: (f2 /. [x1,y1]) - (f2 /. [x0,y0]) = (Q . ((f /. w1) - c)) + ((- 1) * (Q . ((f /. w0) - c))) by A76, A77, A79, A81, RLVECT_1:16
.= (Q . ((f /. w1) - c)) + (Q . ((- 1) * ((f /. w0) - c))) by LOPBAN_1:def 5
.= Q . (((f /. w1) - c) + ((- 1) * ((f /. w0) - c))) by A83
.= Q . ((f /. w1) - (f /. w0)) by A82, RLVECT_1:16 ;
||.Q.|| + 0 < ||.Q.|| + 1 by XREAL_1:8;
then A85: ||.Q.|| * ||.((f /. w1) - (f /. w0)).|| <= (||.Q.|| + 1) * ||.((f /. w1) - (f /. w0)).|| by XREAL_1:64;
||.(Q . ((f /. w1) - (f /. w0))).|| <= ||.Q.|| * ||.((f /. w1) - (f /. w0)).|| by LOPBAN_1:32;
then A86: ||.((f2 /. [x1,y1]) - (f2 /. [x0,y0])).|| <= (||.Q.|| + 1) * ||.((f /. w1) - (f /. w0)).|| by A84, A85, XXREAL_0:2;
- z0 = [(- x0),(- y0)] by A62, PRVECT_3:18;
then z1 - z0 = [(x1 - x0),(y1 - y0)] by A69, PRVECT_3:18;
then ||.(y1 - y0).|| <= ||.(z1 - z0).|| by NORMSP35;
then ||.(y1 - y0).|| < s1 by A68, XXREAL_0:2;
then A88: ||.(y1 - y0).|| < r / 2 by A67, XXREAL_0:2;
(||.Q.|| + 1) * ||.((f /. w1) - (f /. w0)).|| < (||.Q.|| + 1) * (r / (2 * (||.Q.|| + 1))) by A65, A70, A71, A72, XREAL_1:68;
then ||.((f2 /. [x1,y1]) - (f2 /. [x0,y0])).|| < (||.Q.|| + 1) * (r / (2 * (||.Q.|| + 1))) by A86, XXREAL_0:2;
then ||.((f2 /. [x1,y1]) - (f2 /. [x0,y0])).|| < r / 2 by XCMPLX_1:92;
then ||.(y1 - y0).|| + ||.((f2 /. [x1,y1]) - (f2 /. [x0,y0])).|| < (r / 2) + (r / 2) by A88, XREAL_1:8;
hence ||.((Fai /. z1) - (Fai /. z0)).|| < r by A75, XXREAL_0:2; :: thesis:

end;

A89: for w0 being Point of [:E,F:] st w0 in Z holds
f * (reproj2 w0) is_differentiable_in w0 `2

proof

let w0 be Point of [:E,F:]; :: thesis:
assume w0 in Z ; :: thesis:
then f is_partial_differentiable_in`2 w0 by A2, A4;
hence f * (reproj2 w0) is_differentiable_in w0 `2 ; :: thesis:

end;

A90: for w0 being Point of [:E,F:] st w0 in Z holds
ex N being Neighbourhood of w0 `2 st
( N c= dom (f * (reproj2 w0)) & ex R being RestFunc of F,G st
for w1 being Point of F st w1 in N holds
((f * (reproj2 w0)) /. w1) - ((f * (reproj2 w0)) /. (w0 `2)) = ((diff ((f * (reproj2 w0)),(w0 `2))) . (w1 - (w0 `2))) + (R /. (w1 - (w0 `2))) )

proof

let w0 be Point of [:E,F:]; :: thesis:
assume w0 in Z ; :: thesis:
then f * (reproj2 w0) is_differentiable_in w0 `2 by A89;
hence ex N being Neighbourhood of w0 `2 st
( N c= dom (f * (reproj2 w0)) & ex R being RestFunc of F,G st
for w1 being Point of F st w1 in N holds
((f * (reproj2 w0)) /. w1) - ((f * (reproj2 w0)) /. (w0 `2)) = ((diff ((f * (reproj2 w0)),(w0 `2))) . (w1 - (w0 `2))) + (R /. (w1 - (w0 `2))) ) by NDIFF_1:def 7; :: thesis:

end;

A91: for z0 being Point of [:E,F:] st z0 in Z1 holds
( Fai * (reproj2 z0) is_differentiable_in z0 `2 & ex L0, I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( L0 = Q * ((f `partial`2| Z) /. (z0 + e0b)) & I = id the carrier of F & diff ((Fai * (reproj2 z0)),(z0 `2)) = I - L0 ) )

proof

let z0 be Point of [:E,F:]; :: thesis:
assume A92: z0 in Z1 ; :: thesis:
reconsider w0 = z0 + e0b as Point of [:E,F:] ;
consider x0 being Point of E, y0 being Point of F such that
A93: z0 = [x0,y0] by PRVECT_3:18;
consider ww0 being Point of [:E,F:] such that
A94: ( z0 = ww0 - e0b & ww0 in Z ) by A35, A92;
A95: w0 = ww0 - (e0b - e0b) by A94, RLVECT_1:29
.= ww0 - (0. [:E,F:]) by RLVECT_1:15
.= ww0 by RLVECT_1:13 ;
then consider N being Neighbourhood of w0 `2 such that
A96: ( N c= dom (f * (reproj2 w0)) & ex R being RestFunc of F,G st
for w1 being Point of F st w1 in N holds
((f * (reproj2 w0)) /. w1) - ((f * (reproj2 w0)) /. (w0 `2)) = ((diff ((f * (reproj2 w0)),(w0 `2))) . (w1 - (w0 `2))) + (R /. (w1 - (w0 `2))) ) by A90, A94;
consider R being RestFunc of F,G such that
A97: for w1 being Point of F st w1 in N holds
((f * (reproj2 w0)) /. w1) - ((f * (reproj2 w0)) /. (w0 `2)) = ((diff ((f * (reproj2 w0)),(w0 `2))) . (w1 - (w0 `2))) + (R /. (w1 - (w0 `2))) by A96;
reconsider L0 = Q * ((f `partial`2| Z) /. (z0 + e0b)) as Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) ;
id the carrier of F is Lipschitzian LinearOperator of F,F by LOPBAN_2:3;
then reconsider I = id the carrier of F as Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) by LOPBAN_1:def 9;
reconsider L1 = I - L0 as Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) ;
reconsider R0 = Q * R as RestFunc of F,F by NDIFF_2:9;
reconsider R1 = (- 1) (#) R0 as RestFunc of F,F by NDIFF_1:29;
A98: w0 = [(x0 + (0. E)),(y0 + b)] by A93, PRVECT_3:18
.= [x0,(y0 + b)] by RLVECT_1:4 ;
then A99: ( w0 `1 = x0 & w0 `2 = y0 + b ) ;
A100: ( z0 `1 = x0 & z0 `2 = y0 ) by A93;
set N1 = { (z - b) where z is Point of F : z in N } ;
{ (z - b) where z is Point of F : z in N } is Neighbourhood of (y0 + b) - b by A98, NEIB1;
then reconsider N1 = { (z - b) where z is Point of F : z in N } as Neighbourhood of y0 by RLVECT_4:1;

A101: now :: thesis:

let yy1 be object ; :: thesis:
assume A102: yy1 in N1 ; :: thesis:
then reconsider y1 = yy1 as Point of F ;
A103: (reproj2 z0) . y1 = [x0,y1] by A100, NDIFF_7:def 2;
consider w being Point of F such that
A104: ( y1 = w - b & w in N ) by A102;
(reproj2 w0) . w in dom f by A96, A104, FUNCT_1:11;
then A105: [(w0 `1),w] in dom f by NDIFF_7:def 2;
reconsider x0w = [x0,w] as Point of [:E,F:] ;
A106: - e0b = [(- (0. E)),(- b)] by PRVECT_3:18;
[x0,(w - b)] = [(x0 - (0. E)),(w - b)] by RLVECT_1:13
.= x0w - e0b by A106, PRVECT_3:18 ;
then A107: [x0,(w - b)] in Z1 by A2, A35, A98, A105;
dom (reproj2 z0) = the carrier of F by FUNCT_2:def 1;
hence yy1 in dom (Fai * (reproj2 z0)) by A57, A103, A104, A107, FUNCT_1:11; :: thesis:

end;

then A108: N1 c= dom (Fai * (reproj2 z0)) by TARSKI:def 3;

A109: now :: thesis:

let y1 be Point of F; :: thesis:
assume A110: y1 in N1 ; :: thesis:
A111: (reproj2 z0) . y1 = [x0,y1] by A100, NDIFF_7:def 2;
consider w being Point of F such that
A112: ( y1 = w - b & w in N ) by A110;
(reproj2 w0) . w in dom f by A96, A112, FUNCT_1:11;
then A113: [(w0 `1),w] in dom f by NDIFF_7:def 2;
reconsider x0w = [x0,w] as Point of [:E,F:] ;
A114: - e0b = [(- (0. E)),(- b)] by PRVECT_3:18;
[x0,(w - b)] = [(x0 - (0. E)),(w - b)] by RLVECT_1:13
.= x0w - e0b by A114, PRVECT_3:18 ;
then A115: [x0,(w - b)] in Z1 by A2, A35, A98, A113;
dom (reproj2 z0) = the carrier of F by FUNCT_2:def 1;
then A116: y1 in dom (Fai * (reproj2 z0)) by A57, A111, A112, A115, FUNCT_1:11;
A117: (Fai * (reproj2 z0)) /. y1 = (Fai * (reproj2 z0)) . y1 by A116, PARTFUN1:def 6
.= Fai . (x0,y1) by A111, A116, FUNCT_1:12
.= y1 - (f2 /. [x0,y1]) by A58, A112, A115 ;
A118: f2 /. [x0,y1] = f2 . (x0,y1) by A50, A112, A115, PARTFUN1:def 6
.= Q . (f1 . (x0,y1)) by A51, A112, A115 ;
A119: [x0,(y1 + b)] = [x0,w] by A112, RLVECT_4:1;
A120: [x0,w] = (reproj2 w0) . w by A99, NDIFF_7:def 2;
A121: (f * (reproj2 w0)) /. w = (f * (reproj2 w0)) . w by A96, A112, PARTFUN1:def 6
.= f . [x0,(y1 + b)] by A96, A112, A119, A120, FUNCT_1:12
.= f /. [x0,(y1 + b)] by A98, A113, A119, PARTFUN1:def 6 ;
A122: f1 . (x0,y1) = ((f * (reproj2 w0)) /. w) - c by A42, A112, A115, A121;
A123: (reproj2 z0) . y0 = [x0,y0] by A100, NDIFF_7:def 2;
A124: y0 + b in N by A98, NFCONT_1:4;
(reproj2 w0) . (y0 + b) in dom f by A96, A124, FUNCT_1:11;
then A125: [(w0 `1),(y0 + b)] in dom f by NDIFF_7:def 2;
reconsider x0v = [x0,(y0 + b)] as Point of [:E,F:] ;
dom (reproj2 z0) = the carrier of F by FUNCT_2:def 1;
then A126: y0 in dom (Fai * (reproj2 z0)) by A57, A92, A93, A123, FUNCT_1:11;
then A127: (Fai * (reproj2 z0)) /. y0 = (Fai * (reproj2 z0)) . y0 by PARTFUN1:def 6
.= Fai . (x0,y0) by A123, A126, FUNCT_1:12
.= y0 - (f2 /. [x0,y0]) by A58, A92, A93 ;
A128: f2 /. [x0,y0] = f2 . (x0,y0) by A50, A92, A93, PARTFUN1:def 6
.= Q . (f1 . (x0,y0)) by A51, A92, A93 ;
A129: [x0,(y0 + b)] = (reproj2 w0) . (y0 + b) by A99, NDIFF_7:def 2;
A130: (f * (reproj2 w0)) /. (y0 + b) = (f * (reproj2 w0)) . (y0 + b) by A96, A124, PARTFUN1:def 6
.= f . [x0,(y0 + b)] by A96, A124, A129, FUNCT_1:12
.= f /. [x0,(y0 + b)] by A98, A125, PARTFUN1:def 6 ;
A131: f1 . (x0,y0) = ((f * (reproj2 w0)) /. (w0 `2)) - c by A42, A92, A93, A98, A130;
A132: f1 /. [x0,y1] = f1 . (x0,y1) by A41, A112, A115, PARTFUN1:def 6;
A133: f1 /. [x0,y0] = f1 . (x0,y0) by A41, A92, A93, PARTFUN1:def 6;
A134: QQ is additive ;
A135: (f2 /. [x0,y1]) - (f2 /. [x0,y0]) = (Q . (f1 /. [x0,y1])) + ((- 1) * (Q . (f1 /. [x0,y0]))) by A118, A128, A132, A133, RLVECT_1:16
.= (Q . (f1 /. [x0,y1])) + (Q . ((- 1) * (f1 /. [x0,y0]))) by LOPBAN_1:def 5
.= Q . ((f1 /. [x0,y1]) + ((- 1) * (f1 /. [x0,y0]))) by A134
.= Q . ((f1 /. [x0,y1]) - (f1 /. [x0,y0])) by RLVECT_1:16 ;
A136: w - (w0 `2) = y1 - y0 by A98, A112, RLVECT_1:27;
(f1 /. [x0,y1]) - (f1 /. [x0,y0]) = ((((f * (reproj2 w0)) /. w) - c) - ((f * (reproj2 w0)) /. (w0 `2))) + c by A122, A131, A132, A133, RLVECT_1:29
.= (((f * (reproj2 w0)) /. w) - (c + ((f * (reproj2 w0)) /. (w0 `2)))) + c by RLVECT_1:27
.= ((((f * (reproj2 w0)) /. w) - ((f * (reproj2 w0)) /. (w0 `2))) - c) + c by RLVECT_1:27
.= ((f * (reproj2 w0)) /. w) - ((f * (reproj2 w0)) /. (w0 `2)) by RLVECT_4:1
.= ((diff ((f * (reproj2 w0)),(y0 + b))) . (y1 - y0)) + (R /. (y1 - y0)) by A97, A98, A112, A136 ;
then A137: (f2 /. [x0,y1]) - (f2 /. [x0,y0]) = (Q . ((diff ((f * (reproj2 w0)),(y0 + b))) . (y1 - y0))) + (Q . (R /. (y1 - y0))) by A134, A135;
A138: diff ((f * (reproj2 w0)),(y0 + b)) = partdiff`2 (f,w0) by A99, NDIFF_7:def 7
.= (f `partial`2| Z) /. (z0 + e0b) by A4, A94, A95, NDIFF_7:def 11 ;
set Q1 = modetrans (Q,G,F);
set df1 = modetrans ((diff ((f * (reproj2 w0)),(y0 + b))),F,G);
A139: (modetrans (Q,G,F)) * (modetrans ((diff ((f * (reproj2 w0)),(y0 + b))),F,G)) is Lipschitzian LinearOperator of F,F by LOPBAN_2:2;
A140: Q . ((diff ((f * (reproj2 w0)),(y0 + b))) . (y1 - y0)) = Q . ((modetrans ((diff ((f * (reproj2 w0)),(y0 + b))),F,G)) . (y1 - y0)) by LOPBAN_1:def 11
.= (modetrans (Q,G,F)) . ((modetrans ((diff ((f * (reproj2 w0)),(y0 + b))),F,G)) . (y1 - y0)) by LOPBAN_1:def 11
.= (Q * ((f `partial`2| Z) /. (z0 + e0b))) . (y1 - y0) by A138, A139, LPB2Th4 ;
R is total by NDIFF_1:def 5;
then A141: dom R = the carrier of F by PARTFUN1:def 2;
rng R c= the carrier of G ;
then rng R c= dom Q by FUNCT_2:def 1;
then A142: dom (Q * R) = dom R by RELAT_1:27;
A143: dom ((- 1) (#) (QQ * R)) = the carrier of F by A141, A142, VFUNCT_1:def 4;
A144: Q . (R /. (y1 - y0)) = Q . (R . (y1 - y0)) by A141, PARTFUN1:def 6
.= (Q * R) . (y1 - y0) by A141, FUNCT_1:13
.= (QQ * R) /. (y1 - y0) by A141, A142, PARTFUN1:def 6 ;
((Fai * (reproj2 z0)) /. y1) - ((Fai * (reproj2 z0)) /. y0) = ((y1 - (f2 /. [x0,y1])) - y0) + (f2 /. [x0,y0]) by A117, A127, RLVECT_1:29
.= (y1 - ((f2 /. [x0,y1]) + y0)) + (f2 /. [x0,y0]) by RLVECT_1:27
.= ((y1 - y0) - (f2 /. [x0,y1])) + (f2 /. [x0,y0]) by RLVECT_1:27
.= (y1 - y0) - ((L0 . (y1 - y0)) + (R0 /. (y1 - y0))) by A137, A140, A144, RLVECT_1:29
.= ((y1 - y0) - (L0 . (y1 - y0))) - (R0 /. (y1 - y0)) by RLVECT_1:27
.= ((y1 - y0) + (- (L0 . (y1 - y0)))) + ((- 1) * (R0 /. (y1 - y0))) by RLVECT_1:16
.= ((I . (y1 - y0)) - (L0 . (y1 - y0))) + (((- 1) (#) R0) /. (y1 - y0)) by A143, VFUNCT_1:def 4
.= (L1 . (y1 - y0)) + (R1 /. (y1 - y0)) by LOPBAN_1:40 ;
hence ((Fai * (reproj2 z0)) /. y1) - ((Fai * (reproj2 z0)) /. (z0 `2)) = (L1 . (y1 - (z0 `2))) + (R1 /. (y1 - (z0 `2))) by A93; :: thesis:

end;

hence A145: Fai * (reproj2 z0) is_differentiable_in z0 `2 by A93, A101, NDIFF_1:def 6, TARSKI:def 3; :: thesis:
take L0 ; :: thesis:
take I ; :: thesis:
thus ( L0 = Q * ((f `partial`2| Z) /. (z0 + e0b)) & I = id the carrier of F & diff ((Fai * (reproj2 z0)),(z0 `2)) = I - L0 ) by A93, A108, A109, A145, NDIFF_1:def 7; :: thesis:

end;

for z0 being Point of [:E,F:] st z0 in Z1 holds
Fai is_partial_differentiable_in`2 z0 by A91;
then A146: Fai is_partial_differentiable_on`2 Z1 by FUNCT_2:def 1;
A147: ( dom (Fai `partial`2| Z1) = Z1 & ( for z being Point of [:E,F:] st z in Z1 holds
ex L, I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( L = Q * ((f `partial`2| Z) /. (z + e0b)) & I = id the carrier of F & (Fai `partial`2| Z1) /. z = I - L ) ) )

proof

thus dom (Fai `partial`2| Z1) = Z1 by A146, NDIFF_7:def 11; :: thesis:
let z be Point of [:E,F:]; :: thesis:
assume A148: z in Z1 ; :: thesis:
then consider L, I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) such that
A149: ( L = Q * ((f `partial`2| Z) /. (z + e0b)) & I = id the carrier of F & diff ((Fai * (reproj2 z)),(z `2)) = I - L ) by A91;
take L ; :: thesis:
take I ; :: thesis:
thus ( L = Q * ((f `partial`2| Z) /. (z + e0b)) & I = id the carrier of F ) by A149; :: thesis:
thus (Fai `partial`2| Z1) /. z = partdiff`2 (Fai,z) by A146, A148, NDIFF_7:def 11
.= I - L by A149, NDIFF_7:def 7 ; :: thesis:

end;

set FG = Fai `partial`2| Z1;
A150: for z0 being Point of [:E,F:]
for r being Real st z0 in Z1 & 0 < r holds
ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| < r ) )

proof

let z0 be Point of [:E,F:]; :: thesis:
let r be Real; :: thesis:
reconsider w0 = z0 + e0b as Point of [:E,F:] ;
assume A151: ( z0 in Z1 & 0 < r ) ; :: thesis:
then consider ww0 being Point of [:E,F:] such that
A152: ( z0 = ww0 - e0b & ww0 in Z ) by A35;
w0 = ww0 - (e0b - e0b) by A152, RLVECT_1:29
.= ww0 - (0. [:E,F:]) by RLVECT_1:15
.= ww0 by RLVECT_1:13 ;
then consider s being Real such that
A153: ( 0 < s & ( for w1 being Point of [:E,F:] st w1 in Z & ||.(w1 - w0).|| < s holds
||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).|| < r / (||.Q.|| + 1) ) ) by A5, A151, A152, NFCONT_1:19, XREAL_1:139;
take s ; :: thesis:
thus 0 < s by A153; :: thesis:
thus for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| < r :: thesis:

proof

let z1 be Point of [:E,F:]; :: thesis:
reconsider w1 = z1 + e0b as Point of [:E,F:] ;
assume A154: ( z1 in Z1 & ||.(z1 - z0).|| < s ) ; :: thesis:
then consider ww1 being Point of [:E,F:] such that
A155: ( z1 = ww1 - e0b & ww1 in Z ) by A35;
A156: w1 = ww1 - (e0b - e0b) by A155, RLVECT_1:29
.= ww1 - (0. [:E,F:]) by RLVECT_1:15
.= ww1 by RLVECT_1:13 ;
A157: w1 - w0 = ((z1 + e0b) - e0b) - z0 by RLVECT_1:27
.= z1 - z0 by RLVECT_4:1 ;
consider Lz0, Iz0 being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) such that
A158: ( Lz0 = Q * ((f `partial`2| Z) /. (z0 + e0b)) & Iz0 = id the carrier of F & (Fai `partial`2| Z1) /. z0 = Iz0 - Lz0 ) by A147, A151;
consider Lz1, Iz1 being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) such that
A159: ( Lz1 = Q * ((f `partial`2| Z) /. (z1 + e0b)) & Iz1 = id the carrier of F & (Fai `partial`2| Z1) /. z1 = Iz1 - Lz1 ) by A147, A154;
((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0) = ((Iz1 - Lz1) - Iz0) + Lz0 by A158, A159, RLVECT_1:29
.= (Iz1 - (Iz0 + Lz1)) + Lz0 by RLVECT_1:27
.= ((Iz1 - Iz0) - Lz1) + Lz0 by RLVECT_1:27
.= (Iz1 - Iz0) - (Lz1 - Lz0) by RLVECT_1:29
.= (0. (R_NormSpace_of_BoundedLinearOperators (F,F))) - (Lz1 - Lz0) by A158, A159, RLVECT_1:15
.= - (Lz1 - Lz0) by RLVECT_1:14 ;
then A160: ||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| = ||.(Lz1 - Lz0).|| by NORMSP_1:2;
||.Q.|| + 0 < ||.Q.|| + 1 by XREAL_1:8;
then A161: ||.Q.|| * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).|| <= (||.Q.|| + 1) * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).|| by XREAL_1:64;
A162: Q * ((- 1) * ((f `partial`2| Z) /. w0)) = (1 * Q) * ((- 1) * ((f `partial`2| Z) /. w0)) by RLVECT_1:def 8
.= (1 * (- 1)) * (Q * ((f `partial`2| Z) /. w0)) by LPB2Th11
.= - (Q * ((f `partial`2| Z) /. w0)) by RLVECT_1:16 ;
A163: (Q * ((f `partial`2| Z) /. w1)) - (Q * ((f `partial`2| Z) /. w0)) = Q * (((f `partial`2| Z) /. w1) + ((- 1) * ((f `partial`2| Z) /. w0))) by A162, LPB2Th9
.= Q * (((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)) by RLVECT_1:16 ;
set Q1 = modetrans (Q,G,F);
set fp10 = modetrans ((((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)),F,G);
A164: (BoundedLinearOperatorsNorm (G,F)) . (modetrans (Q,G,F)) = ||.Q.|| by LOPBAN_1:def 11;
||.(Lz1 - Lz0).|| <= ((BoundedLinearOperatorsNorm (G,F)) . (modetrans (Q,G,F))) * ((BoundedLinearOperatorsNorm (F,G)) . (modetrans ((((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)),F,G))) by A158, A159, A163, LOPBAN_2:2;
then ||.(Lz1 - Lz0).|| <= ||.Q.|| * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).|| by A164, LOPBAN_1:def 11;
then A165: ||.(Lz1 - Lz0).|| <= (||.Q.|| + 1) * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).|| by A161, XXREAL_0:2;
(||.Q.|| + 1) * ||.(((f `partial`2| Z) /. w1) - ((f `partial`2| Z) /. w0)).|| < (||.Q.|| + 1) * (r / (||.Q.|| + 1)) by A153, A154, A155, A156, A157, XREAL_1:68;
then ||.(Lz1 - Lz0).|| < (||.Q.|| + 1) * (r / (||.Q.|| + 1)) by A165, XXREAL_0:2;
hence ||.(((Fai `partial`2| Z1) /. z1) - ((Fai `partial`2| Z1) /. z0)).|| < r by A160, XCMPLX_1:87; :: thesis:

end;

A166: [a,((0. F) + b)] in Z by A6, RLVECT_1:def 4;
then A167: [a,(0. F)] in Z1 by A21;
A169: Fai . (a,(0. F)) = (0. F) - (f2 /. [a,(0. F)]) by A21, A58, A166;
A168: Fai . (a,(0. F)) = 0. F

proof

f2 /. [a,(0. F)] = f2 . (a,(0. F)) by A21, A50, A166, PARTFUN1:def 6
.= Q . (f1 . (a,(0. F))) by A21, A51, A166
.= Q . ((f /. [a,((0. F) + b)]) - c) by A21, A42, A166
.= Q . ((f /. [a,b]) - c) by RLVECT_1:def 4
.= Q . (c - c) by A2, A6, A7, PARTFUN1:def 6
.= Q . (0. G) by RLVECT_1:15
.= 0. F by LOPBAN_7:3 ;
hence Fai . (a,(0. F)) = 0. F by A169, RLVECT_1:15; :: thesis:

end;

reconsider a0F = [a,(0. F)] as Point of [:E,F:] ;
consider r10 being Real such that
A170: ( 0 < r10 & ( for s being Point of [:E,F:] st s in Z1 & ||.(s - a0F).|| < r10 holds
||.(((Fai `partial`2| Z1) /. s) - ((Fai `partial`2| Z1) /. a0F)).|| < 1 / 4 ) ) by A21, A150, A166;
consider r11 being Real such that
A171: ( 0 < r11 & Ball (a0F,r11) c= Z1 ) by A21, A36, A166, NORMSP27;
reconsider r12 = min (r10,r11) as Real ;
A173: ( r12 <= r11 & r12 <= r10 ) by XXREAL_0:17;
then A174: Ball (a0F,r12) c= Ball (a0F,r11) by LMBALL1;
0 < r12 by A170, A171, XXREAL_0:15;
then consider r1 being Real such that
A175: ( 0 < r1 & r1 < r12 & [:(Ball (a,r1)),(Ball ((0. F),r1)):] c= Ball (a0F,r12) ) by NORMSP31;
[:(Ball (a,r1)),(Ball ((0. F),r1)):] c= Ball (a0F,r11) by A174, A175, XBOOLE_1:1;
then A176: [:(Ball (a,r1)),(Ball ((0. F),r1)):] c= Z1 by A171, XBOOLE_1:1;
A177: for x being Point of [:E,F:] st x in Z1 holds
(Fai `partial`2| Z1) /. x = diff ((Fai * (reproj2 x)),(x `2))

proof

let x be Point of [:E,F:]; :: thesis:
assume x in Z1 ; :: thesis:
hence (Fai `partial`2| Z1) /. x = partdiff`2 (Fai,x) by A146, NDIFF_7:def 11
.= diff ((Fai * (reproj2 x)),(x `2)) by NDIFF_7:def 7 ;
:: thesis:

end;

A179: a in Ball (a,r1) by A175, LMBALL2;
0. F in Ball ((0. F),r1) by A175, LMBALL2;
then A181: [a,(0. F)] in [:(Ball (a,r1)),(Ball ((0. F),r1)):] by A179, ZFMISC_1:87;
reconsider a0F = [a,(0. F)] as Point of [:E,F:] ;
consider La0f, Ia0f being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) such that
A182: ( La0f = Q * ((f `partial`2| Z) /. (a0F + e0b)) & Ia0f = id the carrier of F & (Fai `partial`2| Z1) /. a0F = Ia0f - La0f ) by A147, A176, A181;
partdiff`2 (f,z) is Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
then A183: dom (partdiff`2 (f,z)) = the carrier of F by FUNCT_2:def 1;
A184: Q = modetrans (((partdiff`2 (f,z)) "),G,F) by A10, LOPBAN_1:def 11;
A185: partdiff`2 (f,z) = modetrans ((partdiff`2 (f,z)),F,G) by LOPBAN_1:def 11;
a0F + e0b = [(a + (0. E)),((0. F) + b)] by PRVECT_3:18
.= [a,((0. F) + b)] by RLVECT_1:4
.= z by A6, RLVECT_1:4 ;
then A186: La0f = Q * (partdiff`2 (f,z)) by A4, A6, A182, NDIFF_7:def 11
.= Ia0f by A8, A10, A182, A183, A184, A185, FUNCT_1:39 ;
A187: (Fai `partial`2| Z1) /. [a,(0. F)] = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) by A182, A186, RLVECT_1:15;
A188: for x being Point of E
for y being Point of F st x in Ball (a,r1) & y in Ball ((0. F),r1) holds
||.((Fai `partial`2| Z1) /. [x,y]).|| < 1 / 4

proof

let x be Point of E; :: thesis:
let y be Point of F; :: thesis:
assume ( x in Ball (a,r1) & y in Ball ((0. F),r1) ) ; :: thesis:
then A190: [x,y] in [:(Ball (a,r1)),(Ball ((0. F),r1)):] by ZFMISC_1:87;
reconsider s = [x,y] as Point of [:E,F:] ;
s in Ball (a0F,r12) by A175, A190;
then ex q being Element of [:E,F:] st
( s = q & ||.(a0F - q).|| < r12 ) ;
then ||.(s - a0F).|| < r12 by NORMSP_1:7;
then ||.(s - a0F).|| < r10 by A173, XXREAL_0:2;
then ||.(((Fai `partial`2| Z1) /. s) - ((Fai `partial`2| Z1) /. a0F)).|| < 1 / 4 by A170, A176, A190;
hence ||.((Fai `partial`2| Z1) /. [x,y]).|| < 1 / 4 by A187, RLVECT_1:13; :: thesis:

end;

reconsider r2 = r1 / 2 as Real ;
( 0 < 1 / 2 & 0 < r1 / 2 ) by A175, XREAL_1:215;
then consider ar10 being Real such that
A191: ( 0 < ar10 & ( for s being Point of [:E,F:] st s in Z1 & ||.(s - a0F).|| < ar10 holds
||.((Fai /. s) - (Fai /. a0F)).|| < (1 / 2) * r2 ) ) by A60, A167, XREAL_1:129;
consider ar12 being Real such that
A192: ( 0 < ar12 & ar12 < ar10 & [:(Ball (a,ar12)),(Ball ((0. F),ar12)):] c= Ball (a0F,ar10) ) by A191, NORMSP31;
reconsider ar11 = min (ar10,ar12) as Real ;
A193: 0 < ar11 by A192, XXREAL_0:21;
( ar11 <= ar10 & ar11 <= ar12 ) by XXREAL_0:17;
then A195: Ball (a,ar11) c= Ball (a,ar12) by LMBALL1;
reconsider ar1 = min (ar11,r1) as Real ;
A196: 0 < ar1 by A175, A193, XXREAL_0:21;
A197: ( ar1 <= ar11 & ar1 <= r1 ) by XXREAL_0:17;
then A198: Ball (a,ar1) c= Ball (a,r1) by LMBALL1;
A199: Ball (a,ar1) c= Ball (a,ar11) by A197, LMBALL1;
A200: for x being Point of E st x in Ball (a,ar1) holds
||.(Fai /. [x,(0. F)]).|| <= (1 / 2) * r2

proof

let x be Point of E; :: thesis:
assume A201: x in Ball (a,ar1) ; :: thesis:
0. F in Ball ((0. F),r1) by A175, LMBALL2;
then A202: [x,(0. F)] in [:(Ball (a,r1)),(Ball ((0. F),r1)):] by A198, A201, ZFMISC_1:87;
reconsider x0F = [x,(0. F)] as Point of [:E,F:] ;
A203: x in Ball (a,ar11) by A199, A201;
0. F in Ball ((0. F),ar12) by A192, LMBALL2;
then [x,(0. F)] in [:(Ball (a,ar12)),(Ball ((0. F),ar12)):] by A195, A203, ZFMISC_1:87;
then x0F in Ball (a0F,ar10) by A192;
then ex q being Element of [:E,F:] st
( q = x0F & ||.(a0F - q).|| < ar10 ) ;
then ||.(x0F - a0F).|| < ar10 by NORMSP_1:7;
then A204: ||.((Fai /. x0F) - (Fai /. a0F)).|| < (1 / 2) * r2 by A176, A191, A202;
Fai /. a0F = 0. F by A146, A167, A168, PARTFUN1:def 6;
hence ||.(Fai /. [x,(0. F)]).|| <= (1 / 2) * r2 by A204, RLVECT_1:13; :: thesis:

end;

reconsider r0 = min ((r1 / 2),ar1) as Real ;
A205: 0 < r1 / 2 by A175, XREAL_1:215;
then A206: 0 < r0 by A196, XXREAL_0:21;
A207: r0 <= r1 / 2 by XXREAL_0:17;
r1 / 2 < r1 by A175, XREAL_1:216;
then r0 < r1 by A207, XXREAL_0:2;
then A208: Ball (a,r0) c= Ball (a,r1) by LMBALL1;
A209: for x being Point of E st x in Ball (a,r0) holds
||.(Fai /. [x,(0. F)]).|| <= (1 / 2) * r2

proof

let x be Point of E; :: thesis:
assume A210: x in Ball (a,r0) ; :: thesis:
r0 <= ar1 by XXREAL_0:17;
then Ball (a,r0) c= Ball (a,ar1) by LMBALL1;
hence ||.(Fai /. [x,(0. F)]).|| <= (1 / 2) * r2 by A200, A210; :: thesis:

end;

take r0 ; :: thesis:
take r2 ; :: thesis:
thus ( 0 < r0 & 0 < r2 ) by A196, A205, XXREAL_0:21; :: thesis:
A211: cl_Ball ((0. F),r2) c= Ball ((0. F),r1) by A175, LMBALL1X, XREAL_1:216;
then [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] c= [:(Ball (a,r1)),(Ball ((0. F),r1)):] by A208, ZFMISC_1:96;
then A212: [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] c= Z1 by A176, XBOOLE_1:1;
A213: for x being Point of E st x in Ball (a,r0) holds
for y1, y2 being Point of F st y1 in cl_Ball ((0. F),r2) & y2 in cl_Ball ((0. F),r2) holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= (1 / 2) * ||.(y1 - y2).||

proof

let x be Point of E; :: thesis:
assume A214: x in Ball (a,r0) ; :: thesis:
let y1, y2 be Point of F; :: thesis:
assume that
A215: y1 in cl_Ball ((0. F),r2) and
A216: y2 in cl_Ball ((0. F),r2) ; :: thesis:
A217: [.y1,y2.] c= cl_Ball ((0. F),r2) by A215, A216, LMCLOSE2;
A218: ].y1,y2.[ c= [.y1,y2.] by XBOOLE_1:36;
reconsider s = [x,y1] as Point of [:E,F:] ;
reconsider Fs = Fai * (reproj2 s) as PartFunc of F,F ;
A219: for y being object st y in [.y1,y2.] holds
y in dom Fs

proof

let y be object ; :: thesis:
assume A220: y in [.y1,y2.] ; :: thesis:
then [x,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] by A214, A217, ZFMISC_1:87;
then A221: [x,y] in Z1 by A212;
A222: y in the carrier of F by A220;
s `1 = x ;
then A223: (reproj2 s) . y in Z1 by A220, A221, NDIFF_7:def 2;
y in dom (reproj2 s) by A222, FUNCT_2:def 1;
hence y in dom Fs by A146, A223, FUNCT_1:11; :: thesis:

end;

A224: for y being Point of F st y in [.y1,y2.] holds
Fs is_differentiable_in y

proof

let y be Point of F; :: thesis:
assume y in [.y1,y2.] ; :: thesis:
then A225: [x,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] by A214, A217, ZFMISC_1:87;
reconsider s1 = [x,y] as Point of [:E,F:] ;
A226: Fai * (reproj2 s1) is_differentiable_in s1 `2 by A91, A212, A225;
s1 `1 = s `1 ;
hence Fs is_differentiable_in y by A226, REP2; :: thesis:

end;

A227: for y being Point of F st y in [.y1,y2.] holds
Fs is_continuous_in y by A224, NDIFF_1:44;
A228: for y being Point of F st y in ].y1,y2.[ holds
Fs is_differentiable_in y by A218, A224;
A229: for y being Point of F st y in ].y1,y2.[ holds
||.(diff (Fs,y)).|| <= 1 / 2

proof

let y be Point of F; :: thesis:
assume y in ].y1,y2.[ ; :: thesis:
then A230: y in [.y1,y2.] by A218;
then A231: y in cl_Ball ((0. F),r2) by A217;
A232: [x,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] by A214, A217, A230, ZFMISC_1:87;
reconsider s1 = [x,y] as Point of [:E,F:] ;
||.((Fai `partial`2| Z1) /. [x,y]).|| <= 1 / 4 by A188, A208, A211, A214, A231;
then A233: ||.(diff ((Fai * (reproj2 s1)),(s1 `2))).|| <= 1 / 4 by A177, A212, A232;
s1 `1 = s `1 ;
then Fai * (reproj2 s1) = Fs by REP2;
hence ||.(diff (Fs,y)).|| <= 1 / 2 by A233, XXREAL_0:2; :: thesis:

end;

A234: ||.((Fs /. y2) - (Fs /. y1)).|| <= (1 / 2) * ||.(y2 - y1).|| by A219, A227, A228, A229, NDIFF_5:19, TARSKI:def 3;
( [x,y1] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] & [x,y2] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] ) by A214, A215, A216, ZFMISC_1:87;
then A237: ( [x,y1] in Z1 & [x,y2] in Z1 ) by A212;
A235: dom (reproj2 s) = the carrier of F by FUNCT_2:def 1;
A236: ( y1 in [.y1,y2.] & y2 in [.y1,y2.] ) by RLTOPSP1:68;
then A238: Fs /. y1 = (Fai * (reproj2 s)) . y1 by A219, PARTFUN1:def 6
.= Fai . ((reproj2 s) . y1) by A235, FUNCT_1:13
.= Fai . [(s `1),y1] by NDIFF_7:def 2
.= Fai /. [x,y1] by A146, A237, PARTFUN1:def 6 ;
A239: Fs /. y2 = (Fai * (reproj2 s)) . y2 by A219, A236, PARTFUN1:def 6
.= Fai . ((reproj2 s) . y2) by A235, FUNCT_1:13
.= Fai . [(s `1),y2] by NDIFF_7:def 2
.= Fai /. [x,y2] by A146, A237, PARTFUN1:def 6 ;
||.((Fs /. y2) - (Fs /. y1)).|| = ||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| by A238, A239, NORMSP_1:7;
hence ||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= (1 / 2) * ||.(y1 - y2).|| by A234, NORMSP_1:7; :: thesis:

end;

A240: for x being Point of E
for y being Point of F st x in Ball (a,r0) & y in cl_Ball ((0. F),r2) holds
Fai . (x,y) in cl_Ball ((0. F),r2)

proof

let x be Point of E; :: thesis:
let y be Point of F; :: thesis:
assume A241: ( x in Ball (a,r0) & y in cl_Ball ((0. F),r2) ) ; :: thesis:
then [x,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] by ZFMISC_1:87;
then A242: [x,y] in Z1 by A212;
A243: 0. F in cl_Ball ((0. F),r2) by A205, LMBALL2;
ex p being Point of F st
( p = y & ||.((0. F) - p).|| <= r2 ) by A241;
then ||.(y - (0. F)).|| <= r2 by NORMSP_1:7;
then A244: (1 / 2) * ||.(y - (0. F)).|| <= (1 / 2) * r2 by XREAL_1:64;
A245: ||.(Fai /. [x,(0. F)]).|| <= (1 / 2) * r2 by A209, A241;
||.((Fai /. [x,y]) - (Fai /. [x,(0. F)])).|| <= (1 / 2) * ||.(y - (0. F)).|| by A213, A241, A243;
then A246: ||.((Fai /. [x,y]) - (Fai /. [x,(0. F)])).|| <= (1 / 2) * r2 by A244, XXREAL_0:2;
A247: Fai . (x,y) = Fai /. [x,y] by A146, A242, PARTFUN1:def 6;
then reconsider Fxy = Fai . (x,y) as Point of F ;
Fxy - (0. F) = (Fai /. [x,y]) - ((Fai /. [x,(0. F)]) - (Fai /. [x,(0. F)])) by A247, RLVECT_1:15
.= ((Fai /. [x,y]) - (Fai /. [x,(0. F)])) + (Fai /. [x,(0. F)]) by RLVECT_1:29 ;
then A248: ||.(Fxy - (0. F)).|| <= ||.((Fai /. [x,y]) - (Fai /. [x,(0. F)])).|| + ||.(Fai /. [x,(0. F)]).|| by NORMSP_1:def 1;
||.((Fai /. [x,y]) - (Fai /. [x,(0. F)])).|| + ||.(Fai /. [x,(0. F)]).|| <= ((1 / 2) * r2) + ((1 / 2) * r2) by A245, A246, XREAL_1:7;
then ||.(Fxy - (0. F)).|| <= r2 by A248, XXREAL_0:2;
then ||.((0. F) - Fxy).|| <= r2 by NORMSP_1:7;
hence Fai . (x,y) in cl_Ball ((0. F),r2) ; :: thesis:

end;

A249: [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] c= dom Fai by A212, FUNCT_2:def 1;
A251: Ball (a,r0) <> {} by A206, LMBALL2;
A252: cl_Ball ((0. F),r2) <> {} by A205, LMBALL2;
A253: for y being Point of F st y in cl_Ball ((0. F),r2) holds
for x0 being Point of E st x0 in Ball (a,r0) holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) )

proof

let y be Point of F; :: thesis:
assume A254: y in cl_Ball ((0. F),r2) ; :: thesis:
let x0 be Point of E; :: thesis:
assume x0 in Ball (a,r0) ; :: thesis:
then A257: [x0,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] by A254, ZFMISC_1:87;
reconsider z0 = [x0,y] as Point of [:E,F:] ;
let e be Real; :: thesis:
assume A256: 0 < e ; :: thesis:
consider s being Real such that
A258: ( 0 < s & ( for z1 being Point of [:E,F:] st z1 in Z1 & ||.(z1 - z0).|| < s holds
||.((Fai /. z1) - (Fai /. z0)).|| < e ) ) by A60, A212, A256, A257;
take s ; :: thesis:
thus 0 < s by A258; :: thesis:
let x1 be Point of E; :: thesis:
assume A259: ( x1 in Ball (a,r0) & ||.(x1 - x0).|| < s ) ; :: thesis:
then A260: [x1,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] by A254, ZFMISC_1:87;
reconsider z1 = [x1,y] as Point of [:E,F:] ;
- z0 = [(- x0),(- y)] by PRVECT_3:18;
then z1 - z0 = [(x1 - x0),(y - y)] by PRVECT_3:18
.= [(x1 - x0),(0. F)] by RLVECT_1:15 ;
then ||.(z1 - z0).|| = ||.(x1 - x0).|| by LMNR1;
hence ||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e by A212, A258, A259, A260; :: thesis:

end;

then consider Psi being PartFunc of E,F such that
A262: ( Psi is_continuous_on Ball (a,r0) & dom Psi = Ball (a,r0) & rng Psi c= cl_Ball ((0. F),r2) & ( for x being Point of E st x in Ball (a,r0) holds
Fai . (x,(Psi . x)) = Psi . x ) ) by A213, A240, A249, A251, A252, FIXPOINT3;
for z being object holds
( z in cl_Ball (b,r2) iff z in { (y + b) where y is Point of F : y in cl_Ball ((0. F),r2) } )

proof

let z be object ; :: thesis:

hereby :: thesis:

assume z in cl_Ball (b,r2) ; :: thesis:
then consider p being Point of F such that
A263: ( p = z & ||.(b - p).|| <= r2 ) ;
reconsider y = p - b as Point of F ;
A264: y + b = p - (b - b) by RLVECT_1:29
.= p - (0. F) by RLVECT_1:15
.= p by RLVECT_1:13 ;
||.((0. F) - y).|| = ||.(y - (0. F)).|| by NORMSP_1:7
.= ||.y.|| by RLVECT_1:13 ;
then ||.((0. F) - y).|| <= r2 by A263, NORMSP_1:7;
then y in cl_Ball ((0. F),r2) ;
hence z in { (y + b) where y is Point of F : y in cl_Ball ((0. F),r2) } by A263, A264; :: thesis:

end;

assume z in { (y + b) where y is Point of F : y in cl_Ball ((0. F),r2) } ; :: thesis:
then consider y being Point of F such that
A265: ( z = y + b & y in cl_Ball ((0. F),r2) ) ;
A266: ||.((y + b) - b).|| = ||.(y + (b - b)).|| by RLVECT_1:28
.= ||.(y + (0. F)).|| by RLVECT_1:15
.= ||.y.|| by RLVECT_1:4 ;
ex p being Point of F st
( p = y & ||.((0. F) - p).|| <= r2 ) by A265;
then ||.(y - (0. F)).|| <= r2 by NORMSP_1:7;
then ||.((y + b) - b).|| <= r2 by A266, RLVECT_1:13;
then ||.(b - (y + b)).|| <= r2 by NORMSP_1:7;
hence z in cl_Ball (b,r2) by A265; :: thesis:

end;

then A267: cl_Ball (b,r2) = { (y + b) where y is Point of F : y in cl_Ball ((0. F),r2) } by TARSKI:2;
A268: K .: [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] c= K .: Z1 by A212, RELAT_1:123;
A269: K .: Z1 = H " (H .: Z) by A19, A20, FUNCT_1:85
.= Z by A15, A19, FUNCT_1:94 ;
for y being object holds
( y in [:(Ball (a,r0)),(cl_Ball (b,r2)):] iff ex x being object st
( x in dom K & x in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] & y = K . x ) )

proof

let y be object ; :: thesis:

hereby :: thesis:

assume y in [:(Ball (a,r0)),(cl_Ball (b,r2)):] ; :: thesis:
then consider d, w being object such that
A270: ( d in Ball (a,r0) & w in cl_Ball (b,r2) & y = [d,w] ) by ZFMISC_1:def 2;
reconsider d = d as Point of E by A270;
reconsider w = w as Point of F by A270;
reconsider b2 = w - b as Point of F ;
reconsider p = [d,b2] as Point of [:E,F:] ;
consider y0 being Point of F such that
A271: ( w = y0 + b & y0 in cl_Ball ((0. F),r2) ) by A267, A270;
A272: w - b = y0 + (b - b) by A271, RLVECT_1:28
.= y0 + (0. F) by RLVECT_1:15
.= y0 by RLVECT_1:def 4 ;
then y = [(d + (0. E)),(b2 + b)] by A270, A271, RLVECT_1:def 4
.= p + e0b by PRVECT_3:18
.= (1 * p) + e0b by RLVECT_1:def 8
.= K . p by A16 ;
hence ex x being object st
( x in dom K & x in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] & y = K . x ) by A17, A270, A271, A272, ZFMISC_1:87; :: thesis:

end;

given x being object such that A273: ( x in dom K & x in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] & y = K . x ) ; :: thesis:
reconsider p = x as Point of [:E,F:] by A273;
A274: K . x = (1 * p) + e0b by A16
.= p + e0b by RLVECT_1:def 8 ;
consider z being Point of E, w being Point of F such that
A275: p = [z,w] by PRVECT_3:18;
A276: p + e0b = [(z + (0. E)),(w + b)] by A275, PRVECT_3:18
.= [z,(w + b)] by RLVECT_1:def 4 ;
A277: ( z in Ball (a,r0) & w in cl_Ball ((0. F),r2) ) by A273, A275, ZFMISC_1:87;
then w + b in cl_Ball (b,r2) by A267;
hence y in [:(Ball (a,r0)),(cl_Ball (b,r2)):] by A273, A274, A276, A277, ZFMISC_1:87; :: thesis:

end;

hence [:(Ball (a,r0)),(cl_Ball (b,r2)):] c= Z by A268, A269, FUNCT_1:def 6; :: thesis:
deffunc H₃( object ) -> Element of the carrier of F = (Psi /. $1) + b;
A278: for y being object st y in Ball (a,r0) holds
H₃(y) in cl_Ball (b,r2)

proof

let y be object ; :: thesis:
assume A279: y in Ball (a,r0) ; :: thesis:
reconsider yp = y as Point of E by A279;
Psi . yp in rng Psi by A262, A279, FUNCT_1:3;
then Psi . yp in cl_Ball ((0. F),r2) by A262;
then Psi /. yp in cl_Ball ((0. F),r2) by A262, A279, PARTFUN1:def 6;
hence H₃(y) in cl_Ball (b,r2) by A267; :: thesis:

end;

consider Eta being Function of (Ball (a,r0)),(cl_Ball (b,r2)) such that
A280: for y being object st y in Ball (a,r0) holds
Eta . y = H₃(y) from FUNCT_2:sch 2(A278);
A281: rng Eta c= cl_Ball (b,r2) ;
cl_Ball (b,r2) <> {} by A205, LMBALL2;
then A282: dom Eta = Ball (a,r0) by FUNCT_2:def 1;
rng Eta c= the carrier of F by XBOOLE_1:1;
then reconsider Eta = Eta as PartFunc of E,F by A282, RELSET_1:4;
A284: for x0 being Point of E
for r being Real st x0 in Ball (a,r0) & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < s holds
||.((Eta /. x1) - (Eta /. x0)).|| < r ) )

proof

let x0 be Point of E; :: thesis:
let r be Real; :: thesis:
assume A285: ( x0 in Ball (a,r0) & 0 < r ) ; :: thesis:
then consider s being Real such that
A286: ( 0 < s & ( for x1 being Point of E st x1 in Ball (a,r0) & ||.(x1 - x0).|| < s holds
||.((Psi /. x1) - (Psi /. x0)).|| < r ) ) by A262, NFCONT_1:19;
take s ; :: thesis:
thus 0 < s by A286; :: thesis:
let x1 be Point of E; :: thesis:
assume A287: ( x1 in Ball (a,r0) & ||.(x1 - x0).|| < s ) ; :: thesis:
then A288: Eta /. x1 = Eta . x1 by A282, PARTFUN1:def 6
.= (Psi /. x1) + b by A280, A287 ;
Eta /. x0 = Eta . x0 by A282, A285, PARTFUN1:def 6
.= (Psi /. x0) + b by A280, A285 ;
then (Eta /. x1) - (Eta /. x0) = (((Psi /. x1) + b) - b) - (Psi /. x0) by A288, RLVECT_1:27
.= (Psi /. x1) - (Psi /. x0) by RLVECT_4:1 ;
hence ||.((Eta /. x1) - (Eta /. x0)).|| < r by A286, A287; :: thesis:

end;

A290: for x being Point of E st x in Ball (a,r0) holds
f . (x,(Eta . x)) = c

proof

let x be Point of E; :: thesis:
assume A291: x in Ball (a,r0) ; :: thesis:
then A292: Psi . x in rng Psi by A262, FUNCT_1:3;
then reconsider y = Psi . x as Point of F ;
A293: ( y in cl_Ball ((0. F),r2) & Fai . (x,y) = y ) by A262, A291, A292;
A294: [x,y] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] by A262, A291, A292, ZFMISC_1:87;
then y = y - (f2 /. [x,y]) by A58, A212, A293;
then - (- (f2 /. [x,y])) = - (0. F) by RLVECT_1:9;
then f2 /. [x,y] = - (0. F) by RLVECT_1:17;
then A295: f2 /. [x,y] = 0. F by RLVECT_1:12;
f2 . (x,y) = f2 /. [x,y] by A50, A212, A294, PARTFUN1:def 6;
then A296: Q . (f1 . (x,y)) = 0. F by A51, A212, A294, A295;
f1 . (x,y) = f1 /. [x,y] by A41, A212, A294, PARTFUN1:def 6;
then f1 . (x,y) = 0. G by A8, A10, A296, LQ2;
then 0. G = (f /. [x,(y + b)]) - c by A42, A212, A294;
then A297: f /. [x,(y + b)] = c by RLVECT_1:21;
y + b = (Psi /. x) + b by A262, A291, PARTFUN1:def 6
.= Eta . x by A280, A291 ;
hence f . (x,(Eta . x)) = c by A2, A21, A212, A294, A297, PARTFUN1:def 6; :: thesis:

end;

A298: for x being Point of E st x in Ball (a,r0) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c )

proof

let x be Point of E; :: thesis:
assume A299: x in Ball (a,r0) ; :: thesis:
then A300: Eta . x in rng Eta by A282, FUNCT_1:3;
then reconsider y = Eta . x as Point of F ;
take y ; :: thesis:
thus y in cl_Ball (b,r2) by A281, A300; :: thesis:
thus f . (x,y) = c by A290, A299; :: thesis:

end;

A301: for x being Point of E st x in Ball (a,r0) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2

proof

let x be Point of E; :: thesis:
assume A302: x in Ball (a,r0) ; :: thesis:
let y1, y2 be Point of F; :: thesis:
assume A303: ( y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c ) ; :: thesis:
then consider y10 being Point of F such that
A304: ( y1 = y10 + b & y10 in cl_Ball ((0. F),r2) ) by A267;
consider y20 being Point of F such that
A305: ( y2 = y20 + b & y20 in cl_Ball ((0. F),r2) ) by A267, A303;
A306: [x,y10] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] by A302, A304, ZFMISC_1:87;
A307: [x,y20] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] by A302, A305, ZFMISC_1:87;
A308: [x,y10] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] by A302, A304, ZFMISC_1:87;
A309: [x,y20] in [:(Ball (a,r0)),(cl_Ball ((0. F),r2)):] by A302, A305, ZFMISC_1:87;
f . (x,y1) = f /. [x,y1] by A2, A21, A212, A304, A306, PARTFUN1:def 6;
then (f /. [x,(y10 + b)]) - c = 0. G by A303, A304, RLVECT_1:5;
then f1 . (x,y10) = 0. G by A42, A212, A308;
then Q . (f1 . (x,y10)) = 0. F by LOPBAN_7:3;
then f2 . (x,y10) = 0. F by A51, A212, A308;
then f2 /. [x,y10] = 0. F by A50, A212, A308, PARTFUN1:def 6;
then A311: Fai . (x,y10) = y10 - (0. F) by A58, A212, A308
.= y10 by RLVECT_1:13 ;
f . (x,y2) = f /. [x,y2] by A2, A21, A212, A305, A307, PARTFUN1:def 6;
then (f /. [x,(y20 + b)]) - c = 0. G by A303, A305, RLVECT_1:5;
then f1 . (x,y20) = 0. G by A42, A212, A309;
then Q . (f1 . (x,y20)) = 0. F by LOPBAN_7:3;
then f2 . (x,y20) = 0. F by A51, A212, A309;
then f2 /. [x,y20] = 0. F by A50, A212, A309, PARTFUN1:def 6;
then Fai . (x,y20) = y20 - (0. F) by A58, A212, A309
.= y20 by RLVECT_1:13 ;
hence y1 = y2 by A213, A240, A249, A253, A302, A304, A305, A311, FIXPOINT2; :: thesis:

end;

A313: ( a in Ball (a,r0) & b in cl_Ball (b,r2) ) by A206, A207, LMBALL2;
A314: Eta . a in rng Eta by A206, A282, FUNCT_1:3, LMBALL2;
f . (a,(Eta . a)) = c by A206, A290, LMBALL2;
then A315: Eta . a = b by A7, A281, A301, A313, A314;
for Eta1, Eta2 being PartFunc of E,F st dom Eta1 = Ball (a,r0) & rng Eta1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(Eta1 . x)) = c ) & dom Eta2 = Ball (a,r0) & rng Eta2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(Eta2 . x)) = c ) holds
Eta1 = Eta2

proof

let Eta1, Eta2 be PartFunc of E,F; :: thesis:
assume that
A316: ( dom Eta1 = Ball (a,r0) & rng Eta1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(Eta1 . x)) = c ) ) and
A317: ( dom Eta2 = Ball (a,r0) & rng Eta2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(Eta2 . x)) = c ) ) ; :: thesis:
for x being object st x in dom Eta1 holds
Eta1 . x = Eta2 . x

proof

let x0 be object ; :: thesis:
assume A318: x0 in dom Eta1 ; :: thesis:
then reconsider x = x0 as Point of E ;
A319: Eta1 . x0 in rng Eta1 by A318, FUNCT_1:3;
A320: Eta2 . x0 in rng Eta2 by A316, A317, A318, FUNCT_1:3;
( f . (x,(Eta1 . x)) = c & f . (x,(Eta2 . x)) = c ) by A316, A317, A318;
hence Eta1 . x0 = Eta2 . x0 by A301, A316, A317, A318, A319, A320; :: thesis:

end;

hence Eta1 = Eta2 by A316, A317, FUNCT_1:2; :: thesis:

end;

hence ( ( for x being Point of E st x in Ball (a,r0) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r0) holds
for y1, y2 being Point of F st y1 in cl_Ball (b,r2) & y2 in cl_Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( g is_continuous_on Ball (a,r0) & dom g = Ball (a,r0) & rng g c= cl_Ball (b,r2) & g . a = b & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r0) & rng g1 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r0) & rng g2 c= cl_Ball (b,r2) & ( for x being Point of E st x in Ball (a,r0) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) ) by A281, A282, A284, A290, A298, A301, A315, NFCONT_1:19; :: thesis: