let M be non empty MetrSpace; :: thesis: for f being contraction of M st M is complete holds
ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) )
let f be contraction of M; :: thesis: ( M is complete implies ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) ) )
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 ALI2:def 1;
A4: 1 - L > 0 by A2, XREAL_1:52;
ex S1 being sequence of M st
for n being Element of NAT holds S1 . (n + 1) = f . (S1 . n)

proof

consider z being Element of M;
deffunc H₁( Nat, Element of M) -> Element of the carrier of M = f . $2;
ex h being Function of NAT ,the carrier of M st
( h . 0 = z & ( for n being Nat holds h . (n + 1) = H₁(n,h . n) ) ) from NAT_1:sch 12();
then consider h being Function of NAT ,the carrier of M such that
h . 0 = z and
A5: for n being Nat holds h . (n + 1) = f . (h . n) ;
take h ; :: thesis: for n being Element of NAT holds h . (n + 1) = f . (h . n)
let n be Element of NAT ; :: thesis: h . (n + 1) = f . (h . n)
thus h . (n + 1) = f . (h . n) by A5; :: thesis: verum

end;

then consider S1 being sequence of M such that
A6: for n being Element of NAT holds S1 . (n + 1) = f . (S1 . n) ;
set r = dist (S1 . 1),(S1 . 0 );
A7: 0 <= dist (S1 . 1),(S1 . 0 ) by METRIC_1:5;
A8: 1 - L <> 0 by A2;
assume A9: M is complete ; :: thesis: ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) )

now

per cases ( 0 = dist (S1 . 1),(S1 . 0 ) or 0 <> dist (S1 . 1),(S1 . 0 ) ) ;

suppose A10: 0 = dist (S1 . 1),(S1 . 0 ) ; :: thesis: ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) )

A11: f . (S1 . 0 ) = S1 . (0 + 1) by A6
.= S1 . 0 by A10, METRIC_1:2 ;
for y being Element of M st f . y = y holds
y = S1 . 0

proof

let y be Element of M; :: thesis: ( f . y = y implies y = S1 . 0 )
assume A12: f . y = y ; :: thesis: y = S1 . 0
A13: dist y,(S1 . 0 ) >= 0 by METRIC_1:5;
assume y <> S1 . 0 ; :: thesis: contradiction
then dist y,(S1 . 0 ) <> 0 by METRIC_1:2;
then L * (dist y,(S1 . 0 )) < dist y,(S1 . 0 ) by A2, A13, XREAL_1:159;
hence contradiction by A3, A11, A12; :: thesis: verum

end;

hence ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) ) by A11; :: thesis: verum

end;

suppose A14: 0 <> dist (S1 . 1),(S1 . 0 ) ; :: thesis: ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) )

A15: for n being Element of NAT holds dist (S1 . (n + 1)),(S1 . n) <= (dist (S1 . 1),(S1 . 0 )) * (L to_power n)

proof

defpred S₁[ Element of NAT ] means dist (S1 . ($1 + 1)),(S1 . $1) <= (dist (S1 . 1),(S1 . 0 )) * (L to_power $1);
A16: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume dist (S1 . (k + 1)),(S1 . k) <= (dist (S1 . 1),(S1 . 0 )) * (L to_power k) ; :: thesis: S₁[k + 1]
then A17: L * (dist (S1 . (k + 1)),(S1 . k)) <= L * ((dist (S1 . 1),(S1 . 0 )) * (L to_power k)) by A1, XREAL_1:66;
dist (S1 . ((k + 1) + 1)),(S1 . (k + 1)) = dist (f . (S1 . (k + 1))),(S1 . (k + 1)) by A6
.= dist (f . (S1 . (k + 1))),(f . (S1 . k)) by A6 ;
then A18: dist (S1 . ((k + 1) + 1)),(S1 . (k + 1)) <= L * (dist (S1 . (k + 1)),(S1 . k)) by A3;
L * ((dist (S1 . 1),(S1 . 0 )) * (L to_power k)) = (dist (S1 . 1),(S1 . 0 )) * (L * (L to_power k))
.= (dist (S1 . 1),(S1 . 0 )) * ((L to_power k) * (L to_power 1)) by POWER:30
.= (dist (S1 . 1),(S1 . 0 )) * (L to_power (k + 1)) by A1, POWER:32 ;
hence S₁[k + 1] by A18, A17, XXREAL_0:2; :: thesis: verum

end;

dist (S1 . (0 + 1)),(S1 . 0 ) = (dist (S1 . 1),(S1 . 0 )) * 1
.= (dist (S1 . 1),(S1 . 0 )) * (L to_power 0 ) by POWER:29 ;
then A19: S₁[ 0 ] ;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A19, A16); :: thesis: verum

end;

A20: for k being Element of NAT holds dist (S1 . k),(S1 . 0 ) <= (dist (S1 . 1),(S1 . 0 )) * ((1 - (L to_power k)) / (1 - L))

proof

defpred S₁[ Element of NAT ] means dist (S1 . $1),(S1 . 0 ) <= (dist (S1 . 1),(S1 . 0 )) * ((1 - (L to_power $1)) / (1 - L));
A21: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A22: dist (S1 . k),(S1 . 0 ) <= (dist (S1 . 1),(S1 . 0 )) * ((1 - (L to_power k)) / (1 - L)) ; :: thesis: S₁[k + 1]
dist (S1 . (k + 1)),(S1 . k) <= (dist (S1 . 1),(S1 . 0 )) * (L to_power k) by A15;
then A23: ( dist (S1 . (k + 1)),(S1 . 0 ) <= (dist (S1 . (k + 1)),(S1 . k)) + (dist (S1 . k),(S1 . 0 )) & (dist (S1 . (k + 1)),(S1 . k)) + (dist (S1 . k),(S1 . 0 )) <= ((dist (S1 . 1),(S1 . 0 )) * (L to_power k)) + ((dist (S1 . 1),(S1 . 0 )) * ((1 - (L to_power k)) / (1 - L))) ) by A22, METRIC_1:4, XREAL_1:9;
((dist (S1 . 1),(S1 . 0 )) * (L to_power k)) + ((dist (S1 . 1),(S1 . 0 )) * ((1 - (L to_power k)) / (1 - L))) = (dist (S1 . 1),(S1 . 0 )) * ((L to_power k) + ((1 - (L to_power k)) / (1 - L)))
.= (dist (S1 . 1),(S1 . 0 )) * ((((L to_power k) / (1 - L)) * (1 - L)) + ((1 - (L to_power k)) / (1 - L))) by A8, XCMPLX_1:88
.= (dist (S1 . 1),(S1 . 0 )) * ((((1 - L) * (L to_power k)) / (1 - L)) + ((1 - (L to_power k)) / (1 - L))) by XCMPLX_1:75
.= (dist (S1 . 1),(S1 . 0 )) * ((((1 * (L to_power k)) - (L * (L to_power k))) + (1 - (L to_power k))) / (1 - L)) by XCMPLX_1:63
.= (dist (S1 . 1),(S1 . 0 )) * ((1 - (L * (L to_power k))) / (1 - L))
.= (dist (S1 . 1),(S1 . 0 )) * ((1 - ((L to_power k) * (L to_power 1))) / (1 - L)) by POWER:30
.= (dist (S1 . 1),(S1 . 0 )) * ((1 - (L to_power (k + 1))) / (1 - L)) by A1, POWER:32 ;
hence S₁[k + 1] by A23, XXREAL_0:2; :: thesis: verum

end;

(dist (S1 . 1),(S1 . 0 )) * ((1 - (L to_power 0 )) / (1 - L)) = (dist (S1 . 1),(S1 . 0 )) * ((1 - 1) / (1 - L)) by POWER:29
.= 0 ;
then A24: S₁[ 0 ] by METRIC_1:1;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A24, A21); :: thesis: verum

end;

A25: for k being Element of NAT holds dist (S1 . k),(S1 . 0 ) <= (dist (S1 . 1),(S1 . 0 )) / (1 - L)

proof

let k be Element of NAT ; :: thesis: dist (S1 . k),(S1 . 0 ) <= (dist (S1 . 1),(S1 . 0 )) / (1 - L)
0 < L to_power k by A1, A2, Th2;
then 1 - (L to_power k) <= 1 by XREAL_1:46;
then (1 - (L to_power k)) / (1 - L) <= 1 / (1 - L) by A4, XREAL_1:74;
then A26: (dist (S1 . 1),(S1 . 0 )) * ((1 - (L to_power k)) / (1 - L)) <= (dist (S1 . 1),(S1 . 0 )) * (1 / (1 - L)) by A7, XREAL_1:66;
dist (S1 . k),(S1 . 0 ) <= (dist (S1 . 1),(S1 . 0 )) * ((1 - (L to_power k)) / (1 - L)) by A20;
then dist (S1 . k),(S1 . 0 ) <= (dist (S1 . 1),(S1 . 0 )) * (1 / (1 - L)) by A26, XXREAL_0:2;
hence dist (S1 . k),(S1 . 0 ) <= (dist (S1 . 1),(S1 . 0 )) / (1 - L) by XCMPLX_1:100; :: thesis: verum

end;

A27: for n, k being Element of NAT holds dist (S1 . (n + k)),(S1 . n) <= (L to_power n) * (dist (S1 . k),(S1 . 0 ))

proof

defpred S₁[ Element of NAT ] means for k being Element of NAT holds dist (S1 . ($1 + k)),(S1 . $1) <= (L to_power $1) * (dist (S1 . k),(S1 . 0 ));
A28: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A29: for k being Element of NAT holds dist (S1 . (n + k)),(S1 . n) <= (L to_power n) * (dist (S1 . k),(S1 . 0 )) ; :: thesis: S₁[n + 1]
let k be Element of NAT ; :: thesis: dist (S1 . ((n + 1) + k)),(S1 . (n + 1)) <= (L to_power (n + 1)) * (dist (S1 . k),(S1 . 0 ))
A30: L * ((L to_power n) * (dist (S1 . k),(S1 . 0 ))) = (L * (L to_power n)) * (dist (S1 . k),(S1 . 0 ))
.= ((L to_power n) * (L to_power 1)) * (dist (S1 . k),(S1 . 0 )) by POWER:30
.= (L to_power (n + 1)) * (dist (S1 . k),(S1 . 0 )) by A1, POWER:32 ;
dist (S1 . ((n + 1) + k)),(S1 . (n + 1)) = dist (S1 . ((n + k) + 1)),(S1 . (n + 1))
.= dist (f . (S1 . (n + k))),(S1 . (n + 1)) by A6
.= dist (f . (S1 . (n + k))),(f . (S1 . n)) by A6 ;
then A31: dist (S1 . ((n + 1) + k)),(S1 . (n + 1)) <= L * (dist (S1 . (n + k)),(S1 . n)) by A3;
L * (dist (S1 . (n + k)),(S1 . n)) <= L * ((L to_power n) * (dist (S1 . k),(S1 . 0 ))) by A1, A29, XREAL_1:66;
hence dist (S1 . ((n + 1) + k)),(S1 . (n + 1)) <= (L to_power (n + 1)) * (dist (S1 . k),(S1 . 0 )) by A31, A30, XXREAL_0:2; :: thesis: verum

end;

A32: S₁[ 0 ]

proof

let n be Element of NAT ; :: thesis: dist (S1 . (0 + n)),(S1 . 0 ) <= (L to_power 0 ) * (dist (S1 . n),(S1 . 0 ))
(L to_power 0 ) * (dist (S1 . n),(S1 . 0 )) = 1 * (dist (S1 . n),(S1 . 0 )) by POWER:29
.= dist (S1 . n),(S1 . 0 ) ;
hence dist (S1 . (0 + n)),(S1 . 0 ) <= (L to_power 0 ) * (dist (S1 . n),(S1 . 0 )) ; :: thesis: verum

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A32, A28); :: thesis: verum

end;

A33: for n, k being Element of NAT holds dist (S1 . (n + k)),(S1 . n) <= ((dist (S1 . 1),(S1 . 0 )) / (1 - L)) * (L to_power n)

proof

let n, k be Element of NAT ; :: thesis: dist (S1 . (n + k)),(S1 . n) <= ((dist (S1 . 1),(S1 . 0 )) / (1 - L)) * (L to_power n)
0 <= L to_power n by A1, A2, Th2;
then A34: (L to_power n) * (dist (S1 . k),(S1 . 0 )) <= (L to_power n) * ((dist (S1 . 1),(S1 . 0 )) / (1 - L)) by A25, XREAL_1:66;
dist (S1 . (n + k)),(S1 . n) <= (L to_power n) * (dist (S1 . k),(S1 . 0 )) by A27;
hence dist (S1 . (n + k)),(S1 . n) <= ((dist (S1 . 1),(S1 . 0 )) / (1 - L)) * (L to_power n) by A34, XXREAL_0:2; :: thesis: verum

end;

for s being Real st s > 0 holds
ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist (S1 . (n + k)),(S1 . n) < s

proof

A35: (1 - L) / (dist (S1 . 1),(S1 . 0 )) > 0 by A4, A7, A14, XREAL_1:141;
let s be Real; :: thesis: ( s > 0 implies ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist (S1 . (n + k)),(S1 . n) < s )
assume s > 0 ; :: thesis: ex p being Element of NAT st
for n, k being Element of NAT st p <= n holds
dist (S1 . (n + k)),(S1 . n) < s
then ((1 - L) / (dist (S1 . 1),(S1 . 0 ))) * s > 0 by A35, XREAL_1:131;
then consider p being Element of NAT such that
A36: L to_power p < ((1 - L) / (dist (S1 . 1),(S1 . 0 ))) * s by A1, A2, Th3;
take p ; :: thesis: for n, k being Element of NAT st p <= n holds
dist (S1 . (n + k)),(S1 . n) < s
let n, k be Element of NAT ; :: thesis: ( p <= n implies dist (S1 . (n + k)),(S1 . n) < s )
assume p <= n ; :: thesis: dist (S1 . (n + k)),(S1 . n) < s
then L to_power n <= L to_power p by A1, A2, Th1;
then A37: L to_power n < ((1 - L) / (dist (S1 . 1),(S1 . 0 ))) * s by A36, XXREAL_0:2;
(dist (S1 . 1),(S1 . 0 )) / (1 - L) > 0 by A4, A7, A14, XREAL_1:141;
then A38: ((dist (S1 . 1),(S1 . 0 )) / (1 - L)) * (L to_power n) < ((dist (S1 . 1),(S1 . 0 )) / (1 - L)) * (((1 - L) / (dist (S1 . 1),(S1 . 0 ))) * s) by A37, XREAL_1:70;
A39: dist (S1 . (n + k)),(S1 . n) <= ((dist (S1 . 1),(S1 . 0 )) / (1 - L)) * (L to_power n) by A33;
((dist (S1 . 1),(S1 . 0 )) / (1 - L)) * (((1 - L) / (dist (S1 . 1),(S1 . 0 ))) * s) = (((dist (S1 . 1),(S1 . 0 )) / (1 - L)) * ((1 - L) / (dist (S1 . 1),(S1 . 0 )))) * s
.= (((dist (S1 . 1),(S1 . 0 )) * (1 - L)) / ((dist (S1 . 1),(S1 . 0 )) * (1 - L))) * s by XCMPLX_1:77
.= 1 * s by A8, A14, XCMPLX_1:6, XCMPLX_1:60
.= s ;
hence dist (S1 . (n + k)),(S1 . n) < s by A38, A39, XXREAL_0:2; :: thesis: verum

end;

then S1 is Cauchy by Th8;
then S1 is convergent by A9, Def6;
then consider x being Element of M such that
A40: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist (S1 . m),x < r by Def3;
A41: f . x = x

proof

set a = (dist x,(f . x)) / 4;
assume x <> f . x ; :: thesis: contradiction
then A42: dist x,(f . x) <> 0 by METRIC_1:2;
A43: dist x,(f . x) >= 0 by METRIC_1:5;
then consider n being Element of NAT such that
A44: for m being Element of NAT st n <= m holds
dist (S1 . m),x < (dist x,(f . x)) / 4 by A40, A42, XREAL_1:226;
dist (S1 . (n + 1)),(f . x) = dist (f . (S1 . n)),(f . x) by A6;
then A45: dist (S1 . (n + 1)),(f . x) <= L * (dist (S1 . n),x) by A3;
A46: dist (S1 . n),x < (dist x,(f . x)) / 4 by A44;
L * (dist (S1 . n),x) <= dist (S1 . n),x by A2, METRIC_1:5, XREAL_1:155;
then dist (S1 . (n + 1)),(f . x) <= dist (S1 . n),x by A45, XXREAL_0:2;
then A47: dist (S1 . (n + 1)),(f . x) < (dist x,(f . x)) / 4 by A46, XXREAL_0:2;
A48: ( dist x,(f . x) <= (dist x,(S1 . (n + 1))) + (dist (S1 . (n + 1)),(f . x)) & (dist x,(f . x)) / 2 < dist x,(f . x) ) by A42, A43, METRIC_1:4, XREAL_1:218;
dist x,(S1 . (n + 1)) < (dist x,(f . x)) / 4 by A44, NAT_1:11;
then (dist x,(S1 . (n + 1))) + (dist (S1 . (n + 1)),(f . x)) < ((dist x,(f . x)) / 4) + ((dist x,(f . x)) / 4) by A47, XREAL_1:10;
hence contradiction by A48, XXREAL_0:2; :: thesis: verum

end;

for y being Element of M st f . y = y holds
y = x

proof

let y be Element of M; :: thesis: ( f . y = y implies y = x )
assume A49: f . y = y ; :: thesis: y = x
A50: dist y,x >= 0 by METRIC_1:5;
assume y <> x ; :: thesis: contradiction
then dist y,x <> 0 by METRIC_1:2;
then L * (dist y,x) < dist y,x by A2, A50, XREAL_1:159;
hence contradiction by A3, A41, A49; :: thesis: verum

end;

hence ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) ) by A41; :: thesis: verum

end;

end;

end;

hence ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) ) ; :: thesis: verum