let f be Function of X,X; ( f is contraction implies f is with_unique_fixpoint )
assume A1:
f is contraction
; f is with_unique_fixpoint
set x0 = the Element of the carrier of X;
deffunc H1( set , set ) -> set = f . c2;
consider g being Function such that
A2:
( dom g = NAT & g . 0 = the Element of the carrier of X & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) )
from NAT_1:sch 11();
consider K being Real such that
A3:
0 < K
and
A4:
K < 1
and
A5:
for x, y being Point of X holds ||.((f . x) - (f . y)).|| <= K * ||.(x - y).||
by A1;
defpred S1[ Nat] means g . X in the carrier of X;
A6:
S1[ 0 ]
by A2;
A7:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
g . (k + 1) = f . (g . k)
by A2;
hence
(
S1[
k] implies
S1[
k + 1] )
by FUNCT_2:5;
verum
end;
A8:
for n being Nat holds S1[n]
from NAT_1:sch 2(A6, A7);
for n being object st n in NAT holds
g . n in the carrier of X
by A8;
then reconsider g = g as sequence of X by A2, FUNCT_2:3;
A9:
for n being Nat holds ||.((g . (n + 1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power n)
A17:
for k, n being Nat holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))
A25:
for k, n being Nat holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K))
g is Cauchy_sequence_by_Norm
proof
now for e being Real st e > 0 holds
ex nn being Nat st
for n, m being Nat st n >= nn & m >= nn holds
||.((g . n) - (g . m)).|| < elet e be
Real;
( e > 0 implies ex nn being Nat st
for n, m being Nat st n >= nn & m >= nn holds
||.((g . n) - (g . m)).|| < e )assume A30:
e > 0
;
ex nn being Nat st
for n, m being Nat st n >= nn & m >= nn holds
||.((g . n) - (g . m)).|| < e
e / 2
> 0
by A30, XREAL_1:139;
then consider n being
Nat such that A31:
|.((||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n)).| < e / 2
by Th5, A3, A4;
(||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n) <= |.((||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n)).|
by ABSVALUE:4;
then
(||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n) < e / 2
by A31, XXREAL_0:2;
then A32:
||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) < e / 2
by XCMPLX_1:75;
reconsider nn =
n + 1 as
Nat ;
take nn =
nn;
for n, m being Nat st n >= nn & m >= nn holds
||.((g . n) - (g . m)).|| < enow for m, l being Nat st nn <= m & nn <= l holds
||.((g . l) - (g . m)).|| < elet m,
l be
Nat;
( nn <= m & nn <= l implies ||.((g . l) - (g . m)).|| < e )assume that A33:
nn <= m
and A34:
nn <= l
;
||.((g . l) - (g . m)).|| < eA35:
n < m
by A33, NAT_1:16, XXREAL_0:2;
A36:
n < l
by A34, NAT_1:16, XXREAL_0:2;
consider k1 being
Nat such that A37:
n + k1 = m
by A35, NAT_1:10;
consider k2 being
Nat such that A38:
n + k2 = l
by A36, NAT_1:10;
||.((g . (n + k1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K))
by A25;
then A39:
||.((g . m) - (g . n)).|| < e / 2
by A32, A37, XXREAL_0:2;
||.((g . (n + k2)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K))
by A25;
then
||.((g . l) - (g . n)).|| < e / 2
by A32, A38, XXREAL_0:2;
hence
||.((g . l) - (g . m)).|| < e
by Lm1, A39;
verum end; hence
for
n,
m being
Nat st
n >= nn &
m >= nn holds
||.((g . n) - (g . m)).|| < e
;
verum end;
hence
g is
Cauchy_sequence_by_Norm
by RSSPACE3:8;
verum
end;
then A40:
g is convergent
by LOPBAN_1:def 15;
A41:
lim g = f . (lim g)
set xp = lim g;
A52:
lim g is_a_fixpoint_of f
by A41;
A65:
dom f = the carrier of X
by FUNCT_2:def 1;
take
lim g
; ORDEQ_01:def 1 ( lim g is_a_fixpoint_of f & ( for y being set st y is_a_fixpoint_of f holds
lim g = y ) )
thus
lim g is_a_fixpoint_of f
by A52; for y being set st y is_a_fixpoint_of f holds
lim g = y
let y be set ; ( y is_a_fixpoint_of f implies lim g = y )
assume A66:
y is_a_fixpoint_of f
; lim g = y
then reconsider x1 = lim g, y1 = y as Point of X by A65;
A67:
( f . x1 = x1 & f . y1 = y1 )
by A66, A52;
thus
y = lim g
by A53, A67; verum