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}

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

hence
{x} is closed
; :: thesis: verum
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}

hence lim s1 in {x} by TARSKI:def 1; :: thesis: verum

end;assume A1: ( rng s1 c= {x} & s1 is convergent ) ; :: thesis: lim s1 in {x}

now :: thesis: for n being Nat holds s1 . n = x

then
lim s1 = x
by CLOSE01;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;s1 . n in rng s1 by FUNCT_2:4, ORDINAL1:def 12;

hence s1 . n = x by A1, TARSKI:def 1; :: thesis: verum

hence lim s1 in {x} by TARSKI:def 1; :: thesis: verum