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:50;
ex S1 being sequence of M st
for n being Nat holds S1 . (n + 1) = f . (S1 . n)

proof

set z = the Element of M;
deffunc H₁( Nat, Element of M) -> Element of the carrier of M = f . $2;
ex h being sequence of the carrier of M st
( h . 0 = the Element of M & ( for n being Nat holds h . (n + 1) = H₁(n,h . n) ) ) from NAT_1:sch 12();
then consider h being sequence of the carrier of M such that
h . 0 = the Element of M and
A5: for n being Nat holds h . (n + 1) = f . (h . n) ;
take h ; :: thesis: for n being Nat holds h . (n + 1) = f . (h . n)
let n be 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 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 :: thesis: ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) )

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:157;
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 Nat holds dist ((S1 . (n + 1)),(S1 . n)) <= (dist ((S1 . 1),(S1 . 0))) * (L to_power n)

proof

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

proof

let k be 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:64;
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:25
.= (dist ((S1 . 1),(S1 . 0))) * (L to_power (k + 1)) by A1, POWER:27 ;
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:24 ;
then A19: S₁[ 0 ] ;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A19, A16); :: thesis: verum

end;

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

proof

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

proof

let k be 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:7;
((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:87
.= (dist ((S1 . 1),(S1 . 0))) * ((((1 - L) * (L to_power k)) / (1 - L)) + ((1 - (L to_power k)) / (1 - L))) by XCMPLX_1:74
.= (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:62
.= (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:25
.= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power (k + 1))) / (1 - L)) by A1, POWER:27 ;
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:24
.= 0 ;
then A24: S₁[ 0 ] by METRIC_1:1;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A24, A21); :: thesis: verum

end;

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

proof

let k be 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:44;
then (1 - (L to_power k)) / (1 - L) <= 1 / (1 - L) by A4, XREAL_1:72;
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:64;
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:99; :: thesis: verum

end;

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

proof

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A29: for k being Nat holds dist ((S1 . (n + k)),(S1 . n)) <= (L to_power n) * (dist ((S1 . k),(S1 . 0))) ; :: thesis: S₁[n + 1]
let k be 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:25
.= (L to_power (n + 1)) * (dist ((S1 . k),(S1 . 0))) by A1, POWER:27 ;
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:64;
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 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:24
.= 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 Nat holds S₁[k] from NAT_1:sch 2(A32, A28); :: thesis: verum

end;

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

proof

let n, k be 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:64;
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 Nat st
for n, k being 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:139;
let s be Real; :: thesis: ( s > 0 implies ex p being Nat st
for n, k being Nat st p <= n holds
dist ((S1 . (n + k)),(S1 . n)) < s )
assume s > 0 ; :: thesis: ex p being Nat st
for n, k being 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:129;
then consider p being 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 Nat st p <= n holds
dist ((S1 . (n + k)),(S1 . n)) < s
let n, k be 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:139;
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:68;
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:76
.= 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 Th6;
then S1 is convergent by A9;
then consider x being Element of M such that
A40: for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S1 . m),x) < r ;
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 Nat such that
A44: for m being Nat st n <= m holds
dist ((S1 . m),x) < (dist (x,(f . x))) / 4 by A40, A42, XREAL_1:224;
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:153;
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:216;
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:8;
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:157;
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