let X be RealUnitarySpace; :: thesis: for f being linear-Functional of X st f is Lipschitzian holds
f " {0} is closed
let f be linear-Functional of X; :: thesis: ( f is Lipschitzian implies f " {0} is closed )
assume AS: f is Lipschitzian ; :: thesis: f " {0} is closed
set Y = f " {0};
for s being sequence of X st rng s c= f " {0} & s is convergent holds
lim s in f " {0}

proof

let s be sequence of X; :: thesis: ( rng s c= f " {0} & s is convergent implies lim s in f " {0} )
assume B0: ( rng s c= f " {0} & s is convergent ) ; :: thesis: lim s in f " {0}
reconsider x0 = lim s as Point of X ;
B1: dom f = the carrier of X by FUNCT_2:def 1;
consider K being Real such that
B3: ( 0 < K & ( for x being Point of X holds |.(f . x).| <= K * ||.x.|| ) ) by AS, BHSP_6:def 4;
for x1, x2 being Point of X st x1 in the carrier of X & x2 in the carrier of X holds
|.((f /. x1) - (f /. x2)).| <= K * ||.(x1 - x2).||

proof

let x1, x2 be Point of X; :: thesis: ( x1 in the carrier of X & x2 in the carrier of X implies |.((f /. x1) - (f /. x2)).| <= K * ||.(x1 - x2).|| )
assume ( x1 in the carrier of X & x2 in the carrier of X ) ; :: thesis: |.((f /. x1) - (f /. x2)).| <= K * ||.(x1 - x2).||
C1: |.((f /. x1) - (f /. x2)).| = |.(f . (x1 - x2)).| by HAHNBAN:19;
thus |.((f /. x1) - (f /. x2)).| <= K * ||.(x1 - x2).|| by C1, B3; :: thesis: verum

end;

then f is_Lipschitzian_on the carrier of X by FUNCT_2:def 1, B3;
then B41: f is_continuous_on the carrier of X by LM5;
B5: rng s c= the carrier of X ;
B71: f is_continuous_in x0 by B41;
B91: f /* s = f * s by B1, B5, FUNCT_2:def 11;
ex k being Nat st
for n being Nat st k <= n holds
(f * s) . n = (seq_const 0) . n

proof

set k = the Nat;
C0: for n being Nat st the Nat <= n holds
(f * s) . n = (seq_const 0) . n

proof

let n be Nat; :: thesis: ( the Nat <= n implies (f * s) . n = (seq_const 0) . n )
assume the Nat <= n ; :: thesis: (f * s) . n = (seq_const 0) . n
s . n in rng s by FUNCT_2:4, ORDINAL1:def 12;
then D2: ( s . n in X & f . (s . n) in {0} ) by FUNCT_2:38, B0;
dom s = NAT by FUNCT_2:def 1;
then (f * s) . n in {0} by ORDINAL1:def 12, D2, FUNCT_1:13;
then (f * s) . n = 0 by TARSKI:def 1;
hence (f * s) . n = (seq_const 0) . n by SEQ_1:57; :: thesis: verum

end;

take the Nat ; :: thesis: for n being Nat st the Nat <= n holds
(f * s) . n = (seq_const 0) . n
thus for n being Nat st the Nat <= n holds
(f * s) . n = (seq_const 0) . n by C0; :: thesis: verum

end;

then lim (f * s) = lim (seq_const 0) by SEQ_4:19
.= (seq_const 0) . 0 by SEQ_4:26
.= 0 ;
then f . x0 = 0 by B71, B0, B1, B91;
then ( x0 in X & f . x0 in {0} ) by TARSKI:def 1;
hence lim s in f " {0} by FUNCT_2:38; :: thesis: verum

end;

hence f " {0} is closed by LM1; :: thesis: verum