let X, Y be RealNormSpace; for L being Lipschitzian LinearOperator of X,Y
for seq being sequence of X st L is isomorphism & seq is Cauchy_sequence_by_Norm holds
L * seq is Cauchy_sequence_by_Norm
let L be Lipschitzian LinearOperator of X,Y; for seq being sequence of X st L is isomorphism & seq is Cauchy_sequence_by_Norm holds
L * seq is Cauchy_sequence_by_Norm
let seq be sequence of X; ( L is isomorphism & seq is Cauchy_sequence_by_Norm implies L * seq is Cauchy_sequence_by_Norm )
assume A1:
L is isomorphism
; ( not seq is Cauchy_sequence_by_Norm or L * seq is Cauchy_sequence_by_Norm )
set Lseq = L * seq;
assume A2:
seq is Cauchy_sequence_by_Norm
; L * seq is Cauchy_sequence_by_Norm
for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(((L * seq) . n) - ((L * seq) . m)).|| < r
proof
let r be
Real;
( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(((L * seq) . n) - ((L * seq) . m)).|| < r )
assume
0 < r
;
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(((L * seq) . n) - ((L * seq) . m)).|| < r
then consider k being
Nat such that A3:
for
n,
m being
Nat st
n >= k &
m >= k holds
||.((seq . n) - (seq . m)).|| < r
by A2, RSSPACE3:8;
take
k
;
for n, m being Nat st n >= k & m >= k holds
||.(((L * seq) . n) - ((L * seq) . m)).|| < r
let n,
m be
Nat;
( n >= k & m >= k implies ||.(((L * seq) . n) - ((L * seq) . m)).|| < r )
assume A4:
(
n >= k &
m >= k )
;
||.(((L * seq) . n) - ((L * seq) . m)).|| < r
A5:
dom seq = NAT
by FUNCT_2:def 1;
((L * seq) . n) - ((L * seq) . m) =
(L . (seq . n)) - ((L * seq) . m)
by A5, FUNCT_1:13, ORDINAL1:def 12
.=
(L . (seq . n)) + (- (L . (seq . m)))
by A5, FUNCT_1:13, ORDINAL1:def 12
.=
(L . (seq . n)) + ((- 1) * (L . (seq . m)))
by RLVECT_1:16
.=
(L . (seq . n)) + (L . ((- 1) * (seq . m)))
by LOPBAN_1:def 5
.=
L . ((seq . n) + ((- 1) * (seq . m)))
by VECTSP_1:def 20
.=
L . ((seq . n) - (seq . m))
by RLVECT_1:16
;
then
||.(((L * seq) . n) - ((L * seq) . m)).|| = ||.((seq . n) - (seq . m)).||
by A1;
hence
||.(((L * seq) . n) - ((L * seq) . m)).|| < r
by A3, A4;
verum
end;
hence
L * seq is Cauchy_sequence_by_Norm
by RSSPACE3:8; verum