let S be RealUnitarySpace; :: thesis:
let X be Subset of S; :: thesis:
reconsider Y = X as Subset of (TopSpaceNorm (RUSp2RNSp S)) ;

hereby :: thesis:

assume X is closed Subset of (TopSpaceNorm (RUSp2RNSp S)) ; :: thesis:
then reconsider Y = X as closed Subset of (TopSpaceNorm (RUSp2RNSp S)) ;
A1: for s being sequence of S st ( for n being Nat holds s . n in Y ) & s is convergent holds
lim s in Y by Th11;
thus for s1 being sequence of S st rng s1 c= X & s1 is convergent holds
lim s1 in X :: thesis:

proof

let s1 be sequence of S; :: thesis:
assume that
A2: rng s1 c= X and
A3: s1 is convergent ; :: thesis:

now :: thesis:

let n be Nat; :: thesis:
s1 . n in rng s1 by FUNCT_2:4, ORDINAL1:def 12;
hence s1 . n in X by A2; :: thesis:

end;

hence lim s1 in X by A1, A3; :: thesis:

end;

end;

assume A4: for s1 being sequence of S st rng s1 c= X & s1 is convergent holds
lim s1 in X ; :: thesis:
for s being sequence of S st ( for n being Nat holds s . n in Y ) & s is convergent holds
lim s in Y

proof

let s be sequence of S; :: thesis:
assume that
A5: for n being Nat holds s . n in Y and
A6: s is convergent ; :: thesis:
rng s c= X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng s ; :: thesis:
then consider n being object such that
A7: ( n in dom s & y = s . n ) by FUNCT_1:def 3;
reconsider n = n as Nat by A7;
thus y in X by A7, A5; :: thesis:

end;

hence lim s in Y by A4, A6; :: thesis:

end;

hence X is closed Subset of (TopSpaceNorm (RUSp2RNSp S)) by Th11; :: thesis: