let M be non empty MetrSpace; :: thesis: for f being Contraction of M st TopSpaceMetr M is compact holds

ex c being Point of M st

( f . c = c & ( for x being Point of M st f . x = x holds

x = c ) )

let f be Contraction of M; :: thesis: ( TopSpaceMetr M is compact implies ex c being Point of M st

( f . c = c & ( for x being Point of M st f . x = x holds

x = c ) ) )

set x0 = the Point of M;

set a = dist ( the Point of M,(f . the Point of M));

consider L being Real such that

A1: 0 < L and

A2: L < 1 and

A3: for x, y being Point of M holds dist ((f . x),(f . y)) <= L * (dist (x,y)) by Def1;

assume A4: TopSpaceMetr M is compact ; :: thesis: ex c being Point of M st

( f . c = c & ( for x being Point of M st f . x = x holds

x = c ) )

A48: dist (c,(f . c)) = 0 ;

take c ; :: thesis: ( f . c = c & ( for x being Point of M st f . x = x holds

x = c ) )

thus A49: f . c = c by A48, METRIC_1:2; :: thesis: for x being Point of M st f . x = x holds

x = c

let x be Point of M; :: thesis: ( f . x = x implies x = c )

assume A50: f . x = x ; :: thesis: x = c

A51: dist (x,c) >= 0 by METRIC_1:5;

assume x <> c ; :: thesis: contradiction

then dist (x,c) <> 0 by METRIC_1:2;

then L * (dist (x,c)) < dist (x,c) by A2, A51, XREAL_1:157;

hence contradiction by A3, A49, A50; :: thesis: verum

ex c being Point of M st

( f . c = c & ( for x being Point of M st f . x = x holds

x = c ) )

let f be Contraction of M; :: thesis: ( TopSpaceMetr M is compact implies ex c being Point of M st

( f . c = c & ( for x being Point of M st f . x = x holds

x = c ) ) )

set x0 = the Point of M;

set a = dist ( the Point of M,(f . the Point of M));

consider L being Real such that

A1: 0 < L and

A2: L < 1 and

A3: for x, y being Point of M holds dist ((f . x),(f . y)) <= L * (dist (x,y)) by Def1;

assume A4: TopSpaceMetr M is compact ; :: thesis: ex c being Point of M st

( f . c = c & ( for x being Point of M st f . x = x holds

x = c ) )

now :: thesis: ( dist ( the Point of M,(f . the Point of M)) <> 0 implies ex c being Point of M st dist (c,(f . c)) = 0 )

then consider c being Point of M such that deffunc H_{1}( Nat) -> object = L to_power ($1 + 1);

defpred S_{1}[ set ] means ex n being Nat st $1 = { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) } ;

assume dist ( the Point of M,(f . the Point of M)) <> 0 ; :: thesis: ex c being Point of M st dist (c,(f . c)) = 0

consider F being Subset-Family of (TopSpaceMetr M) such that

A5: for B being Subset of (TopSpaceMetr M) holds

( B in F iff S_{1}[B] )
from SUBSET_1:sch 3();

defpred S_{2}[ Point of M] means dist ($1,(f . $1)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power (0 + 1));

A6: F is closed

A15: { x where x is Point of M : S_{2}[x] } is Subset of M
from DOMAIN_1:sch 7();

F is centered

then consider c9 being Point of (TopSpaceMetr M) such that

A42: c9 in meet F by SUBSET_1:4;

reconsider c = c9 as Point of M by A14;

reconsider dc = dist (c,(f . c)) as Element of REAL by XREAL_0:def 1;

set r = seq_const (dist (c,(f . c)));

consider s9 being Real_Sequence such that

A43: for n being Nat holds s9 . n = H_{1}(n)
from SEQ_1:sch 1();

set s = (dist ( the Point of M,(f . the Point of M))) (#) s9;

lim s9 = 0 by A1, A2, A43, SERIES_1:1;

then A44: lim ((dist ( the Point of M,(f . the Point of M))) (#) s9) = (dist ( the Point of M,(f . the Point of M))) * 0 by A1, A2, A43, SEQ_2:8, SERIES_1:1

.= 0 ;

then A47: lim (seq_const (dist (c,(f . c)))) <= lim ((dist ( the Point of M,(f . the Point of M))) (#) s9) by A45, SEQ_2:18;

(seq_const (dist (c,(f . c)))) . 0 = dist (c,(f . c)) by SEQ_1:57;

then dist (c,(f . c)) <= 0 by A44, A47, SEQ_4:25;

then dist (c,(f . c)) = 0 by METRIC_1:5;

hence ex c being Point of M st dist (c,(f . c)) = 0 ; :: thesis: verum

end;defpred S

assume dist ( the Point of M,(f . the Point of M)) <> 0 ; :: thesis: ex c being Point of M st dist (c,(f . c)) = 0

consider F being Subset-Family of (TopSpaceMetr M) such that

A5: for B being Subset of (TopSpaceMetr M) holds

( B in F iff S

defpred S

A6: F is closed

proof

A14:
TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #)
by PCOMPS_1:def 5;
let B be Subset of (TopSpaceMetr M); :: according to TOPS_2:def 2 :: thesis: ( not B in F or B is closed )

A7: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 5;

then reconsider V = B ` as Subset of M ;

assume B in F ; :: thesis: B is closed

then consider n being Nat such that

A8: B = { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) } by A5;

for x being Point of M st x in V holds

ex r being Real st

( r > 0 & Ball (x,r) c= V )

then B ` is open by A7, PRE_TOPC:def 2;

hence B is closed by TOPS_1:3; :: thesis: verum

end;A7: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 5;

then reconsider V = B ` as Subset of M ;

assume B in F ; :: thesis: B is closed

then consider n being Nat such that

A8: B = { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) } by A5;

for x being Point of M st x in V holds

ex r being Real st

( r > 0 & Ball (x,r) c= V )

proof

then
B ` in Family_open_set M
by PCOMPS_1:def 4;
let x be Point of M; :: thesis: ( x in V implies ex r being Real st

( r > 0 & Ball (x,r) c= V ) )

assume x in V ; :: thesis: ex r being Real st

( r > 0 & Ball (x,r) c= V )

then not x in B by XBOOLE_0:def 5;

then dist (x,(f . x)) > (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A8;

then A9: (dist (x,(f . x))) - ((dist ( the Point of M,(f . the Point of M))) * (L to_power n)) > 0 by XREAL_1:50;

take r = ((dist (x,(f . x))) - ((dist ( the Point of M,(f . the Point of M))) * (L to_power n))) / 2; :: thesis: ( r > 0 & Ball (x,r) c= V )

thus r > 0 by A9, XREAL_1:215; :: thesis: Ball (x,r) c= V

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Ball (x,r) or z in V )

assume A10: z in Ball (x,r) ; :: thesis: z in V

then reconsider y = z as Point of M ;

dist (x,y) < r by A10, METRIC_1:11;

then 2 * (dist (x,y)) < 2 * r by XREAL_1:68;

then A11: (dist (y,(f . y))) + (2 * (dist (x,y))) < (dist (y,(f . y))) + (2 * r) by XREAL_1:6;

(dist (x,y)) + (dist (y,(f . y))) >= dist (x,(f . y)) by METRIC_1:4;

then A12: ((dist (x,y)) + (dist (y,(f . y)))) + (dist ((f . y),(f . x))) >= (dist (x,(f . y))) + (dist ((f . y),(f . x))) by XREAL_1:6;

( dist ((f . y),(f . x)) <= L * (dist (y,x)) & L * (dist (y,x)) <= dist (y,x) ) by A2, A3, METRIC_1:5, XREAL_1:153;

then dist ((f . y),(f . x)) <= dist (y,x) by XXREAL_0:2;

then (dist ((f . y),(f . x))) + (dist (y,x)) <= (dist (y,x)) + (dist (y,x)) by XREAL_1:6;

then A13: (dist (y,(f . y))) + ((dist (y,x)) + (dist ((f . y),(f . x)))) <= (dist (y,(f . y))) + (2 * (dist (y,x))) by XREAL_1:7;

(dist (x,(f . y))) + (dist ((f . y),(f . x))) >= dist (x,(f . x)) by METRIC_1:4;

then ((dist (y,(f . y))) + (dist (x,y))) + (dist ((f . y),(f . x))) >= dist (x,(f . x)) by A12, XXREAL_0:2;

then (dist (y,(f . y))) + (2 * (dist (x,y))) >= dist (x,(f . x)) by A13, XXREAL_0:2;

then ( (dist (x,(f . x))) - (2 * r) = (dist ( the Point of M,(f . the Point of M))) * (L to_power n) & (dist (y,(f . y))) + (2 * r) > dist (x,(f . x)) ) by A11, XXREAL_0:2;

then for x being Point of M holds

( not y = x or not dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) ) by XREAL_1:19;

then not y in B by A8;

hence z in V by A7, SUBSET_1:29; :: thesis: verum

end;( r > 0 & Ball (x,r) c= V ) )

assume x in V ; :: thesis: ex r being Real st

( r > 0 & Ball (x,r) c= V )

then not x in B by XBOOLE_0:def 5;

then dist (x,(f . x)) > (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A8;

then A9: (dist (x,(f . x))) - ((dist ( the Point of M,(f . the Point of M))) * (L to_power n)) > 0 by XREAL_1:50;

take r = ((dist (x,(f . x))) - ((dist ( the Point of M,(f . the Point of M))) * (L to_power n))) / 2; :: thesis: ( r > 0 & Ball (x,r) c= V )

thus r > 0 by A9, XREAL_1:215; :: thesis: Ball (x,r) c= V

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Ball (x,r) or z in V )

assume A10: z in Ball (x,r) ; :: thesis: z in V

then reconsider y = z as Point of M ;

dist (x,y) < r by A10, METRIC_1:11;

then 2 * (dist (x,y)) < 2 * r by XREAL_1:68;

then A11: (dist (y,(f . y))) + (2 * (dist (x,y))) < (dist (y,(f . y))) + (2 * r) by XREAL_1:6;

(dist (x,y)) + (dist (y,(f . y))) >= dist (x,(f . y)) by METRIC_1:4;

then A12: ((dist (x,y)) + (dist (y,(f . y)))) + (dist ((f . y),(f . x))) >= (dist (x,(f . y))) + (dist ((f . y),(f . x))) by XREAL_1:6;

( dist ((f . y),(f . x)) <= L * (dist (y,x)) & L * (dist (y,x)) <= dist (y,x) ) by A2, A3, METRIC_1:5, XREAL_1:153;

then dist ((f . y),(f . x)) <= dist (y,x) by XXREAL_0:2;

then (dist ((f . y),(f . x))) + (dist (y,x)) <= (dist (y,x)) + (dist (y,x)) by XREAL_1:6;

then A13: (dist (y,(f . y))) + ((dist (y,x)) + (dist ((f . y),(f . x)))) <= (dist (y,(f . y))) + (2 * (dist (y,x))) by XREAL_1:7;

(dist (x,(f . y))) + (dist ((f . y),(f . x))) >= dist (x,(f . x)) by METRIC_1:4;

then ((dist (y,(f . y))) + (dist (x,y))) + (dist ((f . y),(f . x))) >= dist (x,(f . x)) by A12, XXREAL_0:2;

then (dist (y,(f . y))) + (2 * (dist (x,y))) >= dist (x,(f . x)) by A13, XXREAL_0:2;

then ( (dist (x,(f . x))) - (2 * r) = (dist ( the Point of M,(f . the Point of M))) * (L to_power n) & (dist (y,(f . y))) + (2 * r) > dist (x,(f . x)) ) by A11, XXREAL_0:2;

then for x being Point of M holds

( not y = x or not dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) ) by XREAL_1:19;

then not y in B by A8;

hence z in V by A7, SUBSET_1:29; :: thesis: verum

then B ` is open by A7, PRE_TOPC:def 2;

hence B is closed by TOPS_1:3; :: thesis: verum

A15: { x where x is Point of M : S

F is centered

proof

then
meet F <> {}
by A4, A6, COMPTS_1:4;
thus
F <> {}
by A5, A14, A15; :: according to FINSET_1:def 3 :: thesis: for b_{1} being set holds

( b_{1} = {} or not b_{1} c= F or not b_{1} is finite or not meet b_{1} = {} )

defpred S_{3}[ Nat] means { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power $1) } <> {} ;

let G be set ; :: thesis: ( G = {} or not G c= F or not G is finite or not meet G = {} )

assume that

A16: G <> {} and

A17: G c= F and

A18: G is finite ; :: thesis: not meet G = {}

G is c=-linear

A33: m in G and

A34: for C being set st C in G holds

m c= C by A16, A18, FINSET_1:11;

A35: m c= meet G by A16, A34, SETFAM_1:5;

A36: for k being Nat st S_{3}[k] holds

S_{3}[k + 1]

.= (dist ( the Point of M,(f . the Point of M))) * (L to_power 0) by POWER:24 ;

then the Point of M in { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power 0) } ;

then A40: S_{3}[ 0 ]
;

A41: for k being Nat holds S_{3}[k]
from NAT_1:sch 2(A40, A36);

m in F by A17, A33;

then m <> {} by A5, A41;

hence not meet G = {} by A35; :: thesis: verum

end;( b

defpred S

let G be set ; :: thesis: ( G = {} or not G c= F or not G is finite or not meet G = {} )

assume that

A16: G <> {} and

A17: G c= F and

A18: G is finite ; :: thesis: not meet G = {}

G is c=-linear

proof

then consider m being set such that
let B, C be set ; :: according to ORDINAL1:def 8 :: thesis: ( not B in G or not C in G or B,C are_c=-comparable )

assume that

A19: B in G and

A20: C in G ; :: thesis: B,C are_c=-comparable

B in F by A17, A19;

then consider n being Nat such that

A21: B = { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) } by A5;

C in F by A17, A20;

then consider m being Nat such that

A22: C = { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power m) } by A5;

A23: for n, m being Nat st n <= m holds

L to_power m <= L to_power n

(dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n)

end;assume that

A19: B in G and

A20: C in G ; :: thesis: B,C are_c=-comparable

B in F by A17, A19;

then consider n being Nat such that

A21: B = { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) } by A5;

C in F by A17, A20;

then consider m being Nat such that

A22: C = { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power m) } by A5;

A23: for n, m being Nat st n <= m holds

L to_power m <= L to_power n

proof

A25:
for n, m being Nat st n <= m holds
let n, m be Nat; :: thesis: ( n <= m implies L to_power m <= L to_power n )

assume A24: n <= m ; :: thesis: L to_power m <= L to_power n

end;assume A24: n <= m ; :: thesis: L to_power m <= L to_power n

(dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n)

proof

A26:
dist ( the Point of M,(f . the Point of M)) >= 0
by METRIC_1:5;

let n, m be Nat; :: thesis: ( n <= m implies (dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) )

assume n <= m ; :: thesis: (dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n)

hence (dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A23, A26, XREAL_1:64; :: thesis: verum

end;let n, m be Nat; :: thesis: ( n <= m implies (dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) )

assume n <= m ; :: thesis: (dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n)

hence (dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A23, A26, XREAL_1:64; :: thesis: verum

now :: thesis: ( ( n <= m & C c= B ) or ( m <= n & B c= C ) )end;

hence
( B c= C or C c= B )
; :: according to XBOOLE_0:def 9 :: thesis: verumper cases
( n <= m or m <= n )
;

end;

case A27:
n <= m
; :: thesis: C c= B

thus
C c= B
:: thesis: verum

end;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in C or y in B )

assume y in C ; :: thesis: y in B

then consider x being Point of M such that

A28: y = x and

A29: dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power m) by A22;

(dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A25, A27;

then dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A29, XXREAL_0:2;

hence y in B by A21, A28; :: thesis: verum

end;assume y in C ; :: thesis: y in B

then consider x being Point of M such that

A28: y = x and

A29: dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power m) by A22;

(dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A25, A27;

then dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A29, XXREAL_0:2;

hence y in B by A21, A28; :: thesis: verum

case A30:
m <= n
; :: thesis: B c= C

thus
B c= C
:: thesis: verum

end;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in B or y in C )

assume y in B ; :: thesis: y in C

then consider x being Point of M such that

A31: y = x and

A32: dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A21;

(dist ( the Point of M,(f . the Point of M))) * (L to_power n) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power m) by A25, A30;

then dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power m) by A32, XXREAL_0:2;

hence y in C by A22, A31; :: thesis: verum

end;assume y in B ; :: thesis: y in C

then consider x being Point of M such that

A31: y = x and

A32: dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A21;

(dist ( the Point of M,(f . the Point of M))) * (L to_power n) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power m) by A25, A30;

then dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power m) by A32, XXREAL_0:2;

hence y in C by A22, A31; :: thesis: verum

A33: m in G and

A34: for C being set st C in G holds

m c= C by A16, A18, FINSET_1:11;

A35: m c= meet G by A16, A34, SETFAM_1:5;

A36: for k being Nat st S

S

proof

dist ( the Point of M,(f . the Point of M)) =
(dist ( the Point of M,(f . the Point of M))) * 1
let k be Nat; :: thesis: ( S_{3}[k] implies S_{3}[k + 1] )

set z = the Element of { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k) } ;

A37: L * ((dist ( the Point of M,(f . the Point of M))) * (L to_power k)) = (dist ( the Point of M,(f . the Point of M))) * (L * (L to_power k))

.= (dist ( the Point of M,(f . the Point of M))) * ((L to_power k) * (L to_power 1)) by POWER:25

.= (dist ( the Point of M,(f . the Point of M))) * (L to_power (k + 1)) by A1, POWER:27 ;

assume { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k) } <> {} ; :: thesis: S_{3}[k + 1]

then the Element of { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k) } in { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k) } ;

then consider y being Point of M such that

y = the Element of { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k) } and

A38: dist (y,(f . y)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k) ;

A39: dist ((f . y),(f . (f . y))) <= L * (dist (y,(f . y))) by A3;

L * (dist (y,(f . y))) <= L * ((dist ( the Point of M,(f . the Point of M))) * (L to_power k)) by A1, A38, XREAL_1:64;

then dist ((f . y),(f . (f . y))) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power (k + 1)) by A37, A39, XXREAL_0:2;

then f . y in { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power (k + 1)) } ;

hence S_{3}[k + 1]
; :: thesis: verum

end;set z = the Element of { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k) } ;

A37: L * ((dist ( the Point of M,(f . the Point of M))) * (L to_power k)) = (dist ( the Point of M,(f . the Point of M))) * (L * (L to_power k))

.= (dist ( the Point of M,(f . the Point of M))) * ((L to_power k) * (L to_power 1)) by POWER:25

.= (dist ( the Point of M,(f . the Point of M))) * (L to_power (k + 1)) by A1, POWER:27 ;

assume { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k) } <> {} ; :: thesis: S

then the Element of { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k) } in { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k) } ;

then consider y being Point of M such that

y = the Element of { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k) } and

A38: dist (y,(f . y)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k) ;

A39: dist ((f . y),(f . (f . y))) <= L * (dist (y,(f . y))) by A3;

L * (dist (y,(f . y))) <= L * ((dist ( the Point of M,(f . the Point of M))) * (L to_power k)) by A1, A38, XREAL_1:64;

then dist ((f . y),(f . (f . y))) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power (k + 1)) by A37, A39, XXREAL_0:2;

then f . y in { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power (k + 1)) } ;

hence S

.= (dist ( the Point of M,(f . the Point of M))) * (L to_power 0) by POWER:24 ;

then the Point of M in { x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power 0) } ;

then A40: S

A41: for k being Nat holds S

m in F by A17, A33;

then m <> {} by A5, A41;

hence not meet G = {} by A35; :: thesis: verum

then consider c9 being Point of (TopSpaceMetr M) such that

A42: c9 in meet F by SUBSET_1:4;

reconsider c = c9 as Point of M by A14;

reconsider dc = dist (c,(f . c)) as Element of REAL by XREAL_0:def 1;

set r = seq_const (dist (c,(f . c)));

consider s9 being Real_Sequence such that

A43: for n being Nat holds s9 . n = H

set s = (dist ( the Point of M,(f . the Point of M))) (#) s9;

lim s9 = 0 by A1, A2, A43, SERIES_1:1;

then A44: lim ((dist ( the Point of M,(f . the Point of M))) (#) s9) = (dist ( the Point of M,(f . the Point of M))) * 0 by A1, A2, A43, SEQ_2:8, SERIES_1:1

.= 0 ;

A45: now :: thesis: for n being Nat holds (seq_const (dist (c,(f . c)))) . n <= ((dist ( the Point of M,(f . the Point of M))) (#) s9) . n

(dist ( the Point of M,(f . the Point of M))) (#) s9 is convergent
by A1, A2, A43, SEQ_2:7, SERIES_1:1;let n be Nat; :: thesis: (seq_const (dist (c,(f . c)))) . n <= ((dist ( the Point of M,(f . the Point of M))) (#) s9) . n

defpred S_{3}[ Point of M] means dist ($1,(f . $1)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power (n + 1));

set B = { x where x is Point of M : S_{3}[x] } ;

{ x where x is Point of M : S_{3}[x] } is Subset of M
from DOMAIN_1:sch 7();

then { x where x is Point of M : S_{3}[x] } in F
by A5, A14;

then c in { x where x is Point of M : S_{3}[x] }
by A42, SETFAM_1:def 1;

then A46: ex x being Point of M st

( c = x & dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power (n + 1)) ) ;

((dist ( the Point of M,(f . the Point of M))) (#) s9) . n = (dist ( the Point of M,(f . the Point of M))) * (s9 . n) by SEQ_1:9

.= (dist ( the Point of M,(f . the Point of M))) * (L to_power (n + 1)) by A43 ;

hence (seq_const (dist (c,(f . c)))) . n <= ((dist ( the Point of M,(f . the Point of M))) (#) s9) . n by A46, SEQ_1:57; :: thesis: verum

end;defpred S

set B = { x where x is Point of M : S

{ x where x is Point of M : S

then { x where x is Point of M : S

then c in { x where x is Point of M : S

then A46: ex x being Point of M st

( c = x & dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power (n + 1)) ) ;

((dist ( the Point of M,(f . the Point of M))) (#) s9) . n = (dist ( the Point of M,(f . the Point of M))) * (s9 . n) by SEQ_1:9

.= (dist ( the Point of M,(f . the Point of M))) * (L to_power (n + 1)) by A43 ;

hence (seq_const (dist (c,(f . c)))) . n <= ((dist ( the Point of M,(f . the Point of M))) (#) s9) . n by A46, SEQ_1:57; :: thesis: verum

then A47: lim (seq_const (dist (c,(f . c)))) <= lim ((dist ( the Point of M,(f . the Point of M))) (#) s9) by A45, SEQ_2:18;

(seq_const (dist (c,(f . c)))) . 0 = dist (c,(f . c)) by SEQ_1:57;

then dist (c,(f . c)) <= 0 by A44, A47, SEQ_4:25;

then dist (c,(f . c)) = 0 by METRIC_1:5;

hence ex c being Point of M st dist (c,(f . c)) = 0 ; :: thesis: verum

A48: dist (c,(f . c)) = 0 ;

take c ; :: thesis: ( f . c = c & ( for x being Point of M st f . x = x holds

x = c ) )

thus A49: f . c = c by A48, METRIC_1:2; :: thesis: for x being Point of M st f . x = x holds

x = c

let x be Point of M; :: thesis: ( f . x = x implies x = c )

assume A50: f . x = x ; :: thesis: x = c

A51: dist (x,c) >= 0 by METRIC_1:5;

assume x <> c ; :: thesis: contradiction

then dist (x,c) <> 0 by METRIC_1:2;

then L * (dist (x,c)) < dist (x,c) by A2, A51, XREAL_1:157;

hence contradiction by A3, A49, A50; :: thesis: verum