let E be RealNormSpace; :: thesis:
let F be RealBanachSpace; :: thesis:
let A be non empty Subset of E; :: thesis:
let B be non empty Subset of F; :: thesis:
let Fai be PartFunc of [:E,F:],F; :: thesis:
assume that
A1: B is closed and
A2: [:A,B:] c= dom Fai and
A3: for x being Point of E
for y being Point of F st x in A & y in B holds
Fai . (x,y) in B and
A4: for y being Point of F st y in B holds
for x0 being Point of E st x0 in A 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 A & ||.(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 A holds
for y1, y2 being Point of F st y1 in B & y2 in B holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) ) ; :: thesis:
thus ex g being PartFunc of E,F st
( g is_continuous_on A & dom g = A & rng g c= B & ( for x being Point of E st x in A holds
Fai . (x,(g . x)) = g . x ) ) :: thesis:

defpred S₁[ object , object ] means ( $2 in B & Fai . ($1,$2) = $2 );
A6: for x, y1, y2 being object st x in A & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 by A1, A2, A3, A4, A5, FIXPOINT2;
A7: for x being object st x in A holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume A8: x in A ; :: thesis:
then reconsider x0 = x as Point of E ;
consider y being Point of F such that
A9: ( y in B & Fai . (x0,y) = y ) by A1, A2, A3, A4, A5, A8, FIXPOINT2;
take y ; :: thesis:
thus S₁[x,y] by A9; :: thesis:

end;

consider g being Function such that
A10: ( dom g = A & ( for x being object st x in A holds
S₁[x,g . x] ) ) from FUNCT_1:sch 2(A6, A7);
A11: rng g c= B

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng g ; :: thesis:
then consider x being object such that
A12: ( x in dom g & y = g . x ) by FUNCT_1:def 3;
thus y in B by A10, A12; :: thesis:

end;

then rng g c= the carrier of F by XBOOLE_1:1;
then g in PFuncs ( the carrier of E, the carrier of F) by A10, PARTFUN1:def 3;
then reconsider g = g as PartFunc of E,F by PARTFUN1:46;
take g ; :: thesis:
for z0 being Point of E
for r being Real st z0 in A & 0 < r holds
ex s being Real st
( 0 < s & ( for z1 being Point of E st z1 in A & ||.(z1 - z0).|| < s holds
||.((g /. z1) - (g /. z0)).|| < r ) )

let z0 be Point of E; :: thesis:
let r be Real; :: thesis:
assume A15: ( z0 in A & 0 < r ) ; :: thesis:
then A16: Fai . (z0,(g . z0)) = g . z0 by A10;
A17: g . z0 in rng g by A10, A15, FUNCT_1:3;
g . z0 = g /. z0 by A10, A15, PARTFUN1:def 6;
then consider s being Real such that
A18: ( 0 < s & ( for x1 being Point of E
for y1 being Point of F st x1 in A & y1 in B & Fai . (x1,y1) = y1 & ||.(x1 - z0).|| < s holds
||.(y1 - (g /. z0)).|| < r ) ) by A1, A2, A3, A4, A5, A11, A15, A16, A17, FIXPOINT2;
take s ; :: thesis:
thus 0 < s by A18; :: thesis:
let z1 be Point of E; :: thesis:
assume A19: ( z1 in A & ||.(z1 - z0).|| < s ) ; :: thesis:
then A20: Fai . (z1,(g . z1)) = g . z1 by A10;
A21: g . z1 in B by A10, A19;
g . z1 = g /. z1 by A10, A19, PARTFUN1:def 6;
hence ||.((g /. z1) - (g /. z0)).|| < r by A18, A19, A20, A21; :: thesis:

end;

end;

let g1, g2 be PartFunc of E,F; :: thesis:
assume A22: ( dom g1 = A & rng g1 c= B & dom g2 = A & rng g2 c= B & ( for x being Point of E st x in A holds
Fai . (x,(g1 . x)) = g1 . x ) & ( for x being Point of E st x in A holds
Fai . (x,(g2 . x)) = g2 . x ) ) ; :: thesis:
for x being object st x in dom g1 holds
g1 . x = g2 . x

let x be object ; :: thesis:
assume A23: x in dom g1 ; :: thesis:
then reconsider y = x as Point of E ;
A24: g1 . y in rng g1 by A23, FUNCT_1:3;
then reconsider z1 = g1 . y as Point of F ;
A25: g2 . y in rng g2 by A22, A23, FUNCT_1:3;
then reconsider z2 = g2 . y as Point of F ;
( Fai . (y,z1) = z1 & Fai . (y,z2) = z2 & z1 in B & z2 in B & y in A ) by A22, A23, A24, A25;
hence g1 . x = g2 . x by A1, A2, A3, A4, A5, FIXPOINT2; :: thesis:

end;