for E being RealNormSpace
for F being RealBanachSpace
for E0 being non empty Subset of E
for F0 being non empty Subset of F
for Fai being PartFunc of [:E,F:],F st F0 is closed & [:E0,F0:] c= dom Fai & ( 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 ) & ( 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 ) ) ) & 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).|| ) ) holds
( ( 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 ) ) ) & ( 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 ) ) ) )