let X, Y be RealNormSpace; :: thesis: for L being Lipschitzian LinearOperator of X,Y
for seq being sequence of X st L is isomorphism holds
( seq is Cauchy_sequence_by_Norm iff 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 holds
( seq is Cauchy_sequence_by_Norm iff L * seq is Cauchy_sequence_by_Norm )

let seq be sequence of X; :: thesis: ( L is isomorphism implies ( seq is Cauchy_sequence_by_Norm iff L * seq is Cauchy_sequence_by_Norm ) )
assume A1: L is isomorphism ; :: thesis: ( seq is Cauchy_sequence_by_Norm iff L * seq is Cauchy_sequence_by_Norm )
A2: dom L = the carrier of X by FUNCT_2:def 1;
set Lseq = L * seq;
thus ( seq is Cauchy_sequence_by_Norm implies L * seq is Cauchy_sequence_by_Norm ) by ; :: thesis: ( L * seq is Cauchy_sequence_by_Norm implies seq is Cauchy_sequence_by_Norm )
assume A3: L * seq is Cauchy_sequence_by_Norm ; :: thesis:
consider K being Lipschitzian LinearOperator of Y,X such that
A4: ( K = L " & K is isomorphism ) by ;
for n being Element of NAT holds (K * (L * seq)) . n = seq . n
proof
let n be Element of NAT ; :: thesis: (K * (L * seq)) . n = seq . n
A5: dom seq = NAT by FUNCT_2:def 1;
dom (L * seq) = NAT by FUNCT_2:def 1;
hence (K * (L * seq)) . n = K . ((L * seq) . n) by FUNCT_1:13
.= (L ") . (L . (seq . n)) by
.= seq . n by ;
:: thesis: verum
end;
then K * (L * seq) = seq ;
hence seq is Cauchy_sequence_by_Norm by ; :: thesis: verum