theorem FIXPOINT2:
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 ) ) ) )