:: deftheorem Def4 defines LinearTopSpaceNorm NORMSP_2:def 4 :
for X being RealNormSpace
for b₂ being non empty strict RLTopStruct holds
( b₂ = LinearTopSpaceNorm X iff ( the carrier of b₂ = the carrier of X & 0. b₂ = 0. X & the addF of b₂ = the addF of X & the Mult of b₂ = the Mult of X & the topology of b₂ = the topology of (TopSpaceNorm X) ) );