now :: thesis: for xt being Point of (LinearTopSpaceNorm X) ex Bt being Basis of st Bt is countable

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;
reconsider Bt = B as Basis of by Th25, Def4;
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