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 ;
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 H1( 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) = H1(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 ;
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 ;
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 S1[ Nat] means dist ((S1 . (\$1 + 1)),(S1 . \$1)) <= (dist ((S1 . 1),(S1 . 0))) * (L to_power \$1);
A16: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume dist ((S1 . (k + 1)),(S1 . k)) <= (dist ((S1 . 1),(S1 . 0))) * (L to_power k) ; :: thesis: S1[k + 1]
then A17: L * (dist ((S1 . (k + 1)),(S1 . k))) <= L * ((dist ((S1 . 1),(S1 . 0))) * (L to_power k)) by ;
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 ;
hence S1[k + 1] by ; :: thesis: verum
end;
dist ((S1 . (0 + 1)),(S1 . 0)) = (dist ((S1 . 1),(S1 . 0))) * 1
.= (dist ((S1 . 1),(S1 . 0))) * () by POWER:24 ;
then A19: S1[ 0 ] ;
thus for k being Nat holds S1[k] from :: 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 S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A22: dist ((S1 . k),(S1 . 0)) <= (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L)) ; :: thesis: S1[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 ;
((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
.= (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 ;
hence S1[k + 1] by ; :: thesis: verum
end;
(dist ((S1 . 1),(S1 . 0))) * ((1 - ()) / (1 - L)) = (dist ((S1 . 1),(S1 . 0))) * ((1 - 1) / (1 - L)) by POWER:24
.= 0 ;
then A24: S1[ 0 ] by METRIC_1:1;
thus for k being Nat holds S1[k] from :: 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 ;
then A26: (dist ((S1 . 1),(S1 . 0))) * ((1 - (L to_power k)) / (1 - L)) <= (dist ((S1 . 1),(S1 . 0))) * (1 / (1 - L)) by ;
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 ;
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 S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[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: S1[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 ;
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 ;
hence dist ((S1 . ((n + 1) + k)),(S1 . (n + 1))) <= (L to_power (n + 1)) * (dist ((S1 . k),(S1 . 0))) by ; :: thesis: verum
end;
A32: S1[ 0 ]
proof
let n be Nat; :: thesis: dist ((S1 . (0 + n)),(S1 . 0)) <= () * (dist ((S1 . n),(S1 . 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)) <= () * (dist ((S1 . n),(S1 . 0))) ; :: thesis: verum
end;
thus for k being Nat holds S1[k] from :: 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 ;
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 ; :: 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 ;
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 ;
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 ;
(dist ((S1 . 1),(S1 . 0))) / (1 - L) > 0 by ;
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 ;
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
.= s ;
hence dist ((S1 . (n + k)),(S1 . n)) < s by ; :: 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 ;
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 ;
then dist ((S1 . (n + 1)),(f . x)) <= dist ((S1 . n),x) by ;
then A47: dist ((S1 . (n + 1)),(f . x)) < (dist (x,(f . x))) / 4 by ;
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 ;
dist (x,(S1 . (n + 1))) < (dist (x,(f . x))) / 4 by ;
then (dist (x,(S1 . (n + 1)))) + (dist ((S1 . (n + 1)),(f . x))) < ((dist (x,(f . x))) / 4) + ((dist (x,(f . x))) / 4) by ;
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 ;
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