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}

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

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

then L /. (lim seq) in {w} by A3, TARSKI:def 1;

hence lim seq in L " {w} by FUNCT_2:38; :: thesis: verum

end;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

then
lim (L /* seq) = w
by CLOSE01;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;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

then L /. (lim seq) in {w} by A3, TARSKI:def 1;

hence lim seq in L " {w} by FUNCT_2:38; :: thesis: verum