let X, Y be RealNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( L is isomorphism & seq is Cauchy_sequence_by_Norm implies L * seq is Cauchy_sequence_by_Norm )

assume A1: L is isomorphism ; :: thesis: ( 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 ; :: thesis: 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

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; :: thesis: 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; :: thesis: ( L is isomorphism & seq is Cauchy_sequence_by_Norm implies L * seq is Cauchy_sequence_by_Norm )

assume A1: L is isomorphism ; :: thesis: ( 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 ; :: thesis: 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

hence
L * seq is Cauchy_sequence_by_Norm
by RSSPACE3:8; :: thesis: verum
let r be Real; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: for n, m being Nat st n >= k & m >= k holds

||.(((L * seq) . n) - ((L * seq) . m)).|| < r

let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.(((L * seq) . n) - ((L * seq) . m)).|| < r )

assume A4: ( n >= k & m >= k ) ; :: thesis: ||.(((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; :: thesis: verum

end;for n, m being Nat st n >= k & m >= k holds

||.(((L * seq) . n) - ((L * seq) . m)).|| < r )

assume 0 < r ; :: thesis: 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 ; :: thesis: for n, m being Nat st n >= k & m >= k holds

||.(((L * seq) . n) - ((L * seq) . m)).|| < r

let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.(((L * seq) . n) - ((L * seq) . m)).|| < r )

assume A4: ( n >= k & m >= k ) ; :: thesis: ||.(((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; :: thesis: verum