A1:
Cl ([#] (LinearTopSpaceNorm X)) = [#] (LinearTopSpaceNorm X)
by TOPS_1:def 3;

[#] (LinearTopSpaceNorm X) = [#] X by NORMSP_2:def 4;

hence [#] X is dense by A1, EQCL1; :: thesis: verum

[#] (LinearTopSpaceNorm X) = [#] X by NORMSP_2:def 4;

hence [#] X is dense by A1, EQCL1; :: thesis: verum