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

proof

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;

hence L * seq is Cauchy_sequence_by_Norm by RSSPACE3:8; :: thesis: verum