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 H1( Nat) -> object = L to_power (\$1 + 1);
defpred S1[ 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 () such that
A5: for B being Subset of () holds
( B in F iff S1[B] ) from defpred S2[ 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 (); :: according to TOPS_2:def 2 :: thesis: ( not B in F or B is closed )
A7: TopSpaceMetr M = TopStruct(# the carrier of 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 ; :: 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 ;
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 ;
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 ;
then (dist (y,(f . y))) + (2 * (dist (x,y))) >= dist (x,(f . x)) by ;
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 ;
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 ; :: thesis: verum
end;
then B ` in Family_open_set M by PCOMPS_1:def 4;
then B ` is open by ;
hence B is closed by TOPS_1:3; :: thesis: verum
end;
A14: TopSpaceMetr M = TopStruct(# the carrier of M,() #) by PCOMPS_1:def 5;
A15: { x where x is Point of M : S2[x] } is Subset of M from F is centered
proof
thus F <> {} by A5, A14, A15; :: according to FINSET_1:def 3 :: thesis: for b1 being set holds
( b1 = {} or not b1 c= F or not b1 is finite or not meet b1 = {} )

defpred S3[ 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 in F by ;
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 ;
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:
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 ; :: 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 ;
then dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by ;
hence y in B by ; :: 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 ;
then dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power m) by ;
hence y in C by ; :: 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 ;
A35: m c= meet G by ;
A36: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[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 ;
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: S3[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 ;
then dist ((f . y),(f . (f . y))) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power (k + 1)) by ;
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 S3[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))) * () 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))) * () } ;
then A40: S3[ 0 ] ;
A41: for k being Nat holds S3[k] from m in F by ;
then m <> {} by ;
hence not meet G = {} by A35; :: thesis: verum
end;
then meet F <> {} by ;
then consider c9 being Point of () 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 = H1(n) from SEQ_1:sch 1();
set s = (dist ( the Point of M,(f . the Point of M))) (#) s9;
lim s9 = 0 by ;
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
.= 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 S3[ 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 : S3[x] } ;
{ x where x is Point of M : S3[x] } is Subset of M from then { x where x is Point of M : S3[x] } in F by ;
then c in { x where x is Point of M : S3[x] } by ;
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 ; :: thesis: verum
end;
(dist ( the Point of M,(f . the Point of M))) (#) s9 is convergent by ;
then A47: lim (seq_const (dist (c,(f . c)))) <= lim ((dist ( the Point of M,(f . the Point of M))) (#) s9) by ;
(seq_const (dist (c,(f . c)))) . 0 = dist (c,(f . c)) by SEQ_1:57;
then dist (c,(f . c)) <= 0 by ;
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 ; :: 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 ;
hence contradiction by A3, A49, A50; :: thesis: verum