let X, Y be RealNormSpace; :: thesis: for L being Function of X,Y
for w being Point of Y st L is_continuous_on the carrier of X holds
L " {w} is closed

let L be Function of X,Y; :: thesis: for w being Point of Y st L is_continuous_on the carrier of X holds
L " {w} is closed

let w be Point of Y; :: thesis: ( L is_continuous_on the carrier of X implies L " {w} is closed )
assume A1: L is_continuous_on the carrier of X ; :: thesis: L " {w} is closed
for seq being sequence of X st rng seq c= L " {w} & seq is convergent holds
lim seq in L " {w}
proof
let seq be sequence of X; :: thesis: ( rng seq c= L " {w} & seq is convergent implies lim seq in L " {w} )
assume A2: ( rng seq c= L " {w} & seq is convergent ) ; :: thesis: lim seq in L " {w}
lim seq in the carrier of X ;
then A3: ( L /* seq is convergent & L /. (lim seq) = lim (L /* seq) ) by ;
now :: thesis: for n being Nat holds (L /* seq) . n = w
let n be Nat; :: thesis: (L /* seq) . n = w
A4: n in NAT by ORDINAL1:def 12;
seq . n in rng seq by ;
then L . (seq . n) in {w} by ;
then L . (seq . n) = w by TARSKI:def 1;
hence (L /* seq) . n = w by ; :: thesis: verum
end;
then lim (L /* seq) = w by CLOSE01;
then L /. (lim seq) in {w} by ;
hence lim seq in L " {w} by FUNCT_2:38; :: thesis: verum
end;
hence L " {w} is closed ; :: thesis: verum