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 A1, A2, NFCONT_1:18;
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 FUNCT_2:4, ORDINAL1:def 12;
then L . (seq . n) in {w} by A2, FUNCT_2:38;
then L . (seq . n) = w by TARSKI:def 1;
hence (L /* seq) . n = w by A4, FUNCT_2:115; :: thesis: verum
end;
then lim (L /* seq) = w by CLOSE01;
then L /. (lim seq) in {w} by A3, TARSKI:def 1;
hence lim seq in L " {w} by FUNCT_2:38; :: thesis: verum
end;
hence L " {w} is closed ; :: thesis: verum