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