let X, Y be RealNormSpace; :: thesis: for L being Lipschitzian LinearOperator of X,Y
for V being Subset of X
for W being Subset of Y st L is isomorphism & W = L .: V & W is closed holds
V is closed

let L be Lipschitzian LinearOperator of X,Y; :: thesis: for V being Subset of X
for W being Subset of Y st L is isomorphism & W = L .: V & W is closed holds
V is closed

let V be Subset of X; :: thesis: for W being Subset of Y st L is isomorphism & W = L .: V & W is closed holds
V is closed

let W be Subset of Y; :: thesis: ( L is isomorphism & W = L .: V & W is closed implies V is closed )
assume A1: ( L is isomorphism & W = L .: V ) ; :: thesis: ( not W is closed or V is closed )
then consider K being Lipschitzian LinearOperator of Y,X such that
A2: ( K = L " & K is isomorphism ) by NISOM01;
A3: dom L = the carrier of X by FUNCT_2:def 1;
assume A4: W is closed ; :: thesis: V is closed
for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
lim s1 in V
proof
let s1 be sequence of X; :: thesis: ( rng s1 c= V & s1 is convergent implies lim s1 in V )
assume A5: ( rng s1 c= V & s1 is convergent ) ; :: thesis: lim s1 in V
set s2 = L * s1;
A6: ( L * s1 is convergent & lim (L * s1) = L . (lim s1) ) by ;
L .: (rng s1) c= L .: V by ;
then rng (L * s1) c= W by ;
then L . (lim s1) in L .: V by A1, A4, A6;
then (L ") . (L . (lim s1)) in K .: (L .: V) by ;
then A8: lim s1 in K .: (L .: V) by ;
A9: K .: (L .: V) = L " (L .: V) by ;
L " (L .: V) c= V by ;
hence lim s1 in V by A8, A9; :: thesis: verum
end;
hence V is closed ; :: thesis: verum