let E be RealNormSpace; :: thesis:
let F be RealBanachSpace; :: thesis:
let E0 be non empty Subset of E; :: thesis:
let F0 be non empty Subset of F; :: thesis:
let Fai be PartFunc of [:E,F:],F; :: thesis:
assume that
A1: F0 is closed and
A2: [:E0,F0:] c= dom Fai and
A3: for x being Point of E
for y being Point of F st x in E0 & y in F0 holds
Fai . (x,y) in F0 and
A4: for y being Point of F st y in F0 holds
for x0 being Point of E st x0 in E0 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 E0 & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) and
A5: ex k being Real st
( 0 < k & k < 1 & ( for x being Point of E st x in E0 holds
for y1, y2 being Point of F st y1 in F0 & y2 in F0 holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) ) ; :: thesis:
consider k being Real such that
A6: ( 0 < k & k < 1 ) and
A7: for x being Point of E st x in E0 holds
for y1, y2 being Point of F st y1 in F0 & y2 in F0 holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| by A5;
thus for x being Point of E st x in E0 holds
( ex y being Point of F st
( y in F0 & Fai . (x,y) = y ) & ( for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds
y1 = y2 ) ) :: thesis:

let x be Point of E; :: thesis:
deffunc H₁( object ) -> set = Fai . (x,$1);
assume A8: x in E0 ; :: thesis:
then A9: for y being object st y in F0 holds
H₁(y) in F0 by A3;
consider Fai0 being Function of F0,F0 such that
A10: for y being object st y in F0 holds
Fai0 . y = H₁(y) from FUNCT_2:sch 2(A9);
A11: rng Fai0 c= F0 ;
A12: dom Fai0 = F0 by FUNCT_2:def 1;
rng Fai0 c= the carrier of F by XBOOLE_1:1;
then reconsider Fai0 = Fai0 as PartFunc of F,F by A12, RELSET_1:4;
A13: for z, y being Point of F st z in F0 & y in F0 holds
||.((Fai0 /. z) - (Fai0 /. y)).|| <= k * ||.(z - y).||

let z, y be Point of F; :: thesis:
assume A14: ( z in F0 & y in F0 ) ; :: thesis:
then A15: [x,z] in [:E0,F0:] by A8, ZFMISC_1:87;
A16: [x,y] in [:E0,F0:] by A8, A14, ZFMISC_1:87;
A18: y in dom Fai0 by A14, FUNCT_2:def 1;
z in dom Fai0 by A14, FUNCT_2:def 1;
then A19: Fai0 /. z = Fai0 . z by PARTFUN1:def 6
.= H₁(z) by A10, A14
.= Fai /. [x,z] by A2, A15, PARTFUN1:def 6 ;
Fai0 /. y = Fai0 . y by A18, PARTFUN1:def 6
.= H₁(y) by A10, A14
.= Fai /. [x,y] by A2, A16, PARTFUN1:def 6 ;
hence ||.((Fai0 /. z) - (Fai0 /. y)).|| <= k * ||.(z - y).|| by A7, A8, A14, A19; :: thesis:

end;

thus ex y being Point of F st
( y in F0 & Fai . (x,y) = y ) :: thesis:

proof

consider y being Point of F such that
A20: ( y in F0 & Fai0 . y = y ) by A1, A6, A11, A12, A13, FIXPOINT;
take y ; :: thesis:
thus y in F0 by A20; :: thesis:
thus Fai . (x,y) = y by A10, A20; :: thesis:

end;

thus for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds
y1 = y2 :: thesis:

proof

let y1, y2 be Point of F; :: thesis:
assume A21: ( y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 ) ; :: thesis:
A22: Fai0 . y1 = y1 by A10, A21;
Fai0 . y2 = y2 by A10, A21;
hence y1 = y2 by A1, A6, A11, A12, A13, A21, A22, FIXPOINT; :: thesis:

end;

thus for x0 being Point of E
for y0 being Point of F st x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) ) :: thesis:

proof

let x0 be Point of E; :: thesis:
let y0 be Point of F; :: thesis:
assume A24: ( x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 ) ; :: thesis:
let e be Real; :: thesis:
assume A25: 0 < e ; :: thesis:
reconsider e1 = e * (1 - k) as Real ;
A26: 0 < 1 - k by A6, XREAL_1:50;
then consider d being Real such that
A27: ( 0 < d & ( for x1 being Point of E st x1 in E0 & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y0]) - (Fai /. [x0,y0])).|| < e1 ) ) by A4, A24, A25, XREAL_1:129;
take d ; :: thesis:
thus 0 < d by A27; :: thesis:
let x1 be Point of E; :: thesis:
let y1 be Point of F; :: thesis:
assume A28: ( x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d ) ; :: thesis:
[x0,y0] in [:E0,F0:] by A24, ZFMISC_1:87;
then A29: y0 = Fai /. [x0,y0] by A2, A24, PARTFUN1:def 6;
[x1,y1] in [:E0,F0:] by A28, ZFMISC_1:87;
then A30: y1 = Fai /. [x1,y1] by A2, A28, PARTFUN1:def 6;
((Fai /. [x1,y1]) - (Fai /. [x1,y0])) + ((Fai /. [x1,y0]) - (Fai /. [x0,y0])) = (((Fai /. [x1,y1]) - (Fai /. [x1,y0])) + (Fai /. [x1,y0])) - (Fai /. [x0,y0]) by RLVECT_1:28
.= (Fai /. [x1,y1]) - (Fai /. [x0,y0]) by RLVECT_4:1 ;
then A31: ||.(y1 - y0).|| <= ||.((Fai /. [x1,y1]) - (Fai /. [x1,y0])).|| + ||.((Fai /. [x1,y0]) - (Fai /. [x0,y0])).|| by A29, A30, NORMSP_1:def 1;
||.((Fai /. [x1,y0]) - (Fai /. [x0,y0])).|| < e1 by A27, A28;
then ||.((Fai /. [x1,y1]) - (Fai /. [x1,y0])).|| + ||.((Fai /. [x1,y0]) - (Fai /. [x0,y0])).|| < e1 + (k * ||.(y1 - y0).||) by A7, A24, A28, XREAL_1:8;
then ||.(y1 - y0).|| < e1 + (k * ||.(y1 - y0).||) by A31, XXREAL_0:2;
then ||.(y1 - y0).|| - (k * ||.(y1 - y0).||) < (e1 + (k * ||.(y1 - y0).||)) - (k * ||.(y1 - y0).||) by XREAL_1:14;
then (1 - k) * ||.(y1 - y0).|| < e1 ;
then ||.(y1 - y0).|| < e1 / (1 - k) by A26, XREAL_1:81;
hence ||.(y1 - y0).|| < e by A26, XCMPLX_1:89; :: thesis:

end;