now

let xt be Point of (LinearTopSpaceNorm X); :: thesis: ex Bt being Basis of st Bt is countable
reconsider x = xt as Point of (TopSpaceNorm X) by Def4;
consider B being Basis of such that
A1: B is countable by FRECHET:def 2;
B is Subset-Family of (LinearTopSpaceNorm X) by Def4;
then reconsider Bt = B as Basis of by Th25;
take Bt = Bt; :: thesis: Bt is countable
thus Bt is countable by A1; :: thesis: verum

end;

hence LinearTopSpaceNorm X is first-countable by FRECHET:def 2; :: thesis: verum