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 A5, NISOM02;
L .: (rng s1) c= L .: V by A5, RELAT_1:123;
then rng (L * s1) c= W by A1, RELAT_1:127;
then L . (lim s1) in L .: V by A1, A4, A6;
then (L ") . (L . (lim s1)) in K .: (L .: V) by A2, FUNCT_2:35;
then A8: lim s1 in K .: (L .: V) by A1, A3, FUNCT_1:34;
A9: K .: (L .: V) = L " (L .: V) by A1, A2, FUNCT_1:85;
L " (L .: V) c= V by A1, FUNCT_1:82;
hence lim s1 in V by A8, A9; :: thesis: verum

end;

hence V is closed ; :: thesis: verum