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 ) )

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 )

deffunc H₁( Nat) -> object = L to_power ($1 + 1);
defpred S₁[ 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₁[B] ) from SUBSET_1:sch 3();
defpred S₂[ 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

proof

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 )

proof

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;

then B ` in Family_open_set M by PCOMPS_1:def 4;
then B ` is open by A7, PRE_TOPC:def 2;
hence B is closed by TOPS_1:3; :: thesis: verum

end;

A14: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 5;
A15: { x where x is Point of M : S₂[x] } is Subset of M from DOMAIN_1:sch 7();
F is centered

proof

thus F <> {} by A5, A14, A15; :: according to FINSET_1:def 3 :: thesis: for b₁ being set holds
( b₁ = {} or not b₁ c= F or not b₁ is finite or not meet b₁ = {} )
defpred S₃[ 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

proof

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

proof

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

per cases ( n < m or n = m ) by A24, XXREAL_0:1;

suppose n < m ; :: thesis: L to_power m <= L to_power n

hence L to_power m <= L to_power n by A1, A2, POWER:40; :: thesis: verum

end;

suppose n = m ; :: thesis: L to_power m <= L to_power n

hence L to_power m <= L to_power n ; :: thesis: verum

end;

end;

end;

A25: for n, m being Nat st n <= m holds
(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;

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

per cases ( n <= m or m <= n ) ;

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

thus C c= B :: thesis: verum

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;

end;

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

thus B c= C :: thesis: verum

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;

end;

end;

end;

hence ( B c= C or C c= B ) ; :: according to XBOOLE_0:def 9 :: thesis: verum

end;

then consider m being set such that
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₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis: ( S₃[k] implies S₃[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₃[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₃[k + 1] ; :: thesis: verum

end;

dist ( the Point of M,(f . the Point of M)) = (dist ( the Point of M,(f . the Point of M))) * 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₃[ 0 ] ;
A41: for k being Nat holds S₃[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;

then meet F <> {} by A4, A6, COMPTS_1:4;
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₁(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 ;

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

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₃[ 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₃[x] } ;
{ x where x is Point of M : S₃[x] } is Subset of M from DOMAIN_1:sch 7();
then { x where x is Point of M : S₃[x] } in F by A5, A14;
then c in { x where x is Point of M : S₃[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;

(dist ( the Point of M,(f . the Point of M))) (#) s9 is convergent by A1, A2, A43, SEQ_2:7, SERIES_1:1;
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;

then consider c being Point of M such that
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