let X be RealNormSpace; :: thesis: for x being Point of X holds {x} is closed
let x be Point of X; :: thesis: {x} is closed
for s1 being sequence of X st rng s1 c= {x} & s1 is convergent holds
lim s1 in {x}
proof
let s1 be sequence of X; :: thesis: ( rng s1 c= {x} & s1 is convergent implies lim s1 in {x} )
assume A1: ( rng s1 c= {x} & s1 is convergent ) ; :: thesis: lim s1 in {x}
now :: thesis: for n being Nat holds s1 . n = x
let n be Nat; :: thesis: s1 . n = x
s1 . n in rng s1 by FUNCT_2:4, ORDINAL1:def 12;
hence s1 . n = x by A1, TARSKI:def 1; :: thesis: verum
end;
then lim s1 = x by CLOSE01;
hence lim s1 in {x} by TARSKI:def 1; :: thesis: verum
end;
hence {x} is closed ; :: thesis: verum