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

hence seq is Cauchy_sequence_by_Norm by A3, A4, NISOM04; :: thesis: verum

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

then
K * (L * seq) = seq
;
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;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

hence seq is Cauchy_sequence_by_Norm by A3, A4, NISOM04; :: thesis: verum