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 & L < 1 ) and
A2: for x, y being Point of M holds dist (f . x),(f . y) <= L * (dist x,y) by ALI2:def 1;
A3: 1 - L > 0 by A1, XREAL_1:52;
A4: 1 - L <> 0 by A1;
assume A5: 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 ) )
ex S1 being sequence of M st
for n being Element of NAT holds S1 . (n + 1) = f . (S1 . n)

proof

deffunc H₁( Nat, Element of M) -> Element of the carrier of M = f . $2;
consider z being Element of M;
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
A6: ( h . 0 = z & ( 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 A6; :: thesis: verum

end;

then consider S1 being sequence of M such that
A7: for n being Element of NAT holds S1 . (n + 1) = f . (S1 . n) ;
set r = dist (S1 . 1),(S1 . 0 );
A8: 0 <= dist (S1 . 1),(S1 . 0 ) by METRIC_1:5;

now

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

suppose A9: 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 ) )

A10: f . (S1 . 0 ) = S1 . (0 + 1) by A7
.= S1 . 0 by A9, 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 A11: f . y = y ; :: thesis: y = S1 . 0
assume y <> S1 . 0 ; :: thesis: contradiction
then A12: dist y,(S1 . 0 ) <> 0 by METRIC_1:2;
dist y,(S1 . 0 ) >= 0 by METRIC_1:5;
then L * (dist y,(S1 . 0 )) < dist y,(S1 . 0 ) by A1, A12, XREAL_1:159;
hence contradiction by A2, A10, A11; :: 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 A10; :: thesis: verum

end;

suppose A13: 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 ) )

A14: 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);
A15: S₁[ 0 ]

proof

dist (S1 . (0 + 1)),(S1 . 0 ) = (dist (S1 . 1),(S1 . 0 )) * 1
.= (dist (S1 . 1),(S1 . 0 )) * (L to_power 0 ) by POWER:29 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

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 A17: dist (S1 . (k + 1)),(S1 . k) <= (dist (S1 . 1),(S1 . 0 )) * (L to_power k) ; :: thesis: S₁[k + 1]
dist (S1 . ((k + 1) + 1)),(S1 . (k + 1)) = dist (f . (S1 . (k + 1))),(S1 . (k + 1)) by A7
.= dist (f . (S1 . (k + 1))),(f . (S1 . k)) by A7 ;
then A18: dist (S1 . ((k + 1) + 1)),(S1 . (k + 1)) <= L * (dist (S1 . (k + 1)),(S1 . k)) by A2;
A19: L * (dist (S1 . (k + 1)),(S1 . k)) <= L * ((dist (S1 . 1),(S1 . 0 )) * (L to_power k)) by A1, A17, XREAL_1:66;
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, A19, XXREAL_0:2; :: thesis: verum

end;

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

end;

A20: 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 ));
A21: 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;

A22: 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 A23: 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 ))
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 A7
.= dist (f . (S1 . (n + k))),(f . (S1 . n)) by A7 ;
then A24: dist (S1 . ((n + 1) + k)),(S1 . (n + 1)) <= L * (dist (S1 . (n + k)),(S1 . n)) by A2;
A25: L * (dist (S1 . (n + k)),(S1 . n)) <= L * ((L to_power n) * (dist (S1 . k),(S1 . 0 ))) by A1, A23, XREAL_1:66;
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 ;
hence dist (S1 . ((n + 1) + k)),(S1 . (n + 1)) <= (L to_power (n + 1)) * (dist (S1 . k),(S1 . 0 )) by A24, A25, XXREAL_0:2; :: thesis: verum

end;

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

end;

A26: 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));
A27: S₁[ 0 ]

proof

(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 ;
hence S₁[ 0 ] by METRIC_1:1; :: thesis: verum

end;

A28: 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 A29: dist (S1 . k),(S1 . 0 ) <= (dist (S1 . 1),(S1 . 0 )) * ((1 - (L to_power k)) / (1 - L)) ; :: thesis: S₁[k + 1]
A30: dist (S1 . (k + 1)),(S1 . 0 ) <= (dist (S1 . (k + 1)),(S1 . k)) + (dist (S1 . k),(S1 . 0 )) by METRIC_1:4;
dist (S1 . (k + 1)),(S1 . k) <= (dist (S1 . 1),(S1 . 0 )) * (L to_power k) by A14;
then A31: (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 A29, 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 A4, 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 A30, A31, XXREAL_0:2; :: thesis: verum

end;

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

end;

A32: 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)
A33: dist (S1 . k),(S1 . 0 ) <= (dist (S1 . 1),(S1 . 0 )) * ((1 - (L to_power k)) / (1 - L)) by A26;
( L to_power k <= 1 & 0 < L to_power k ) by A1, Th2;
then 1 - (L to_power k) <= 1 by XREAL_1:46;
then (1 - (L to_power k)) / (1 - L) <= 1 / (1 - L) by A3, XREAL_1:74;
then (dist (S1 . 1),(S1 . 0 )) * ((1 - (L to_power k)) / (1 - L)) <= (dist (S1 . 1),(S1 . 0 )) * (1 / (1 - L)) by A8, XREAL_1:66;
then dist (S1 . k),(S1 . 0 ) <= (dist (S1 . 1),(S1 . 0 )) * (1 / (1 - L)) by A33, XXREAL_0:2;
hence dist (S1 . k),(S1 . 0 ) <= (dist (S1 . 1),(S1 . 0 )) / (1 - L) by XCMPLX_1:100; :: thesis: verum

end;

A34: 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)
A35: dist (S1 . (n + k)),(S1 . n) <= (L to_power n) * (dist (S1 . k),(S1 . 0 )) by A20;
0 <= L to_power n by A1, Th2;
then (L to_power n) * (dist (S1 . k),(S1 . 0 )) <= (L to_power n) * ((dist (S1 . 1),(S1 . 0 )) / (1 - L)) by A32, XREAL_1:66;
hence dist (S1 . (n + k)),(S1 . n) <= ((dist (S1 . 1),(S1 . 0 )) / (1 - L)) * (L to_power n) by A35, XXREAL_0:2; :: thesis: verum

end;

S1 is Cauchy

proof

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

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 A36: 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
A37: (dist (S1 . 1),(S1 . 0 )) / (1 - L) > 0 by A3, A8, A13, XREAL_1:141;
(1 - L) / (dist (S1 . 1),(S1 . 0 )) > 0 by A3, A8, A13, XREAL_1:141;
then ((1 - L) / (dist (S1 . 1),(S1 . 0 ))) * s > 0 by A36, XREAL_1:131;
then consider p being Element of NAT such that
A38: L to_power p < ((1 - L) / (dist (S1 . 1),(S1 . 0 ))) * s by A1, 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, Th1;
then L to_power n < ((1 - L) / (dist (S1 . 1),(S1 . 0 ))) * s by A38, XXREAL_0:2;
then A39: ((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;
A40: dist (S1 . (n + k)),(S1 . n) <= ((dist (S1 . 1),(S1 . 0 )) / (1 - L)) * (L to_power n) by A34;
((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 A4, A13, XCMPLX_1:6, XCMPLX_1:60
.= s ;
hence dist (S1 . (n + k)),(S1 . n) < s by A39, A40, XXREAL_0:2; :: thesis: verum

end;

hence S1 is Cauchy by Th8; :: thesis: verum

end;

then S1 is convergent by A5, Def6;
then consider x being Element of M such that
A41: 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;
A42: f . x = x

proof

assume x <> f . x ; :: thesis: contradiction
then A43: dist x,(f . x) <> 0 by METRIC_1:2;
A44: dist x,(f . x) >= 0 by METRIC_1:5;
then A45: 0 < (dist x,(f . x)) / 4 by A43, XREAL_1:226;
set a = (dist x,(f . x)) / 4;
consider n being Element of NAT such that
A46: for m being Element of NAT st n <= m holds
dist (S1 . m),x < (dist x,(f . x)) / 4 by A41, A45;
A47: dist x,(S1 . (n + 1)) < (dist x,(f . x)) / 4 by A46, NAT_1:11;
dist (S1 . (n + 1)),(f . x) = dist (f . (S1 . n)),(f . x) by A7;
then A48: dist (S1 . (n + 1)),(f . x) <= L * (dist (S1 . n),x) by A2;
A49: dist (S1 . n),x < (dist x,(f . x)) / 4 by A46;
dist (S1 . n),x >= 0 by METRIC_1:5;
then L * (dist (S1 . n),x) <= dist (S1 . n),x by A1, XREAL_1:155;
then dist (S1 . (n + 1)),(f . x) <= dist (S1 . n),x by A48, XXREAL_0:2;
then dist (S1 . (n + 1)),(f . x) < (dist x,(f . x)) / 4 by A49, XXREAL_0:2;
then A50: (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;
A51: dist x,(f . x) <= (dist x,(S1 . (n + 1))) + (dist (S1 . (n + 1)),(f . x)) by METRIC_1:4;
(dist x,(f . x)) / 2 < dist x,(f . x) by A43, A44, XREAL_1:218;
hence contradiction by A50, A51, 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 A52: f . y = y ; :: thesis: y = x
assume y <> x ; :: thesis: contradiction
then A53: dist y,x <> 0 by METRIC_1:2;
dist y,x >= 0 by METRIC_1:5;
then L * (dist y,x) < dist y,x by A1, A53, XREAL_1:159;
hence contradiction by A2, A42, A52; :: 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 A42; :: 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