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 convergent iff L * seq is convergent )

let L be Lipschitzian LinearOperator of X,Y; :: thesis: for seq being sequence of X st L is isomorphism holds

( seq is convergent iff L * seq is convergent )

let seq be sequence of X; :: thesis: ( L is isomorphism implies ( seq is convergent iff L * seq is convergent ) )

assume A1: L is isomorphism ; :: thesis: ( seq is convergent iff L * seq is convergent )

A2: dom L = the carrier of X by FUNCT_2:def 1;

set Lseq = L * seq;

set Ls = L . (lim seq);

thus ( seq is convergent implies L * seq is convergent ) by NISOM02; :: thesis: ( L * seq is convergent implies seq is convergent )

assume A3: L * seq is convergent ; :: thesis: seq is convergent

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 convergent by A3, NISOM02; :: thesis: verum

for seq being sequence of X st L is isomorphism holds

( seq is convergent iff L * seq is convergent )

let L be Lipschitzian LinearOperator of X,Y; :: thesis: for seq being sequence of X st L is isomorphism holds

( seq is convergent iff L * seq is convergent )

let seq be sequence of X; :: thesis: ( L is isomorphism implies ( seq is convergent iff L * seq is convergent ) )

assume A1: L is isomorphism ; :: thesis: ( seq is convergent iff L * seq is convergent )

A2: dom L = the carrier of X by FUNCT_2:def 1;

set Lseq = L * seq;

set Ls = L . (lim seq);

thus ( seq is convergent implies L * seq is convergent ) by NISOM02; :: thesis: ( L * seq is convergent implies seq is convergent )

assume A3: L * seq is convergent ; :: thesis: seq is convergent

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 convergent by A3, NISOM02; :: thesis: verum