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 A1, NISOM04; :: 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: seq is Cauchy_sequence_by_Norm
consider K being Lipschitzian LinearOperator of Y,X such that
A4: ( K = L " & K is isomorphism ) by A1, NISOM01;
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 A4, A5, FUNCT_1:13
.= seq . n by A1, A2, FUNCT_1:34 ;
:: thesis: verum

end;

then K * (L * seq) = seq ;
hence seq is Cauchy_sequence_by_Norm by A3, A4, NISOM04; :: thesis: verum