let V be RealNormSpace; :: thesis: for V1 being SubRealNormSpace of V holds LinearTopSpaceNorm V1 is SubSpace of LinearTopSpaceNorm V
let V1 be SubRealNormSpace of V; :: thesis: LinearTopSpaceNorm V1 is SubSpace of LinearTopSpaceNorm V
( the carrier of (LinearTopSpaceNorm V1) = the carrier of V1 & the carrier of (LinearTopSpaceNorm V) = the carrier of V ) by NORMSP_2:def 4;
then ( TopStruct(# the carrier of (LinearTopSpaceNorm V1), the topology of (LinearTopSpaceNorm V1) #) = TopStruct(# the carrier of (TopSpaceNorm V1), the topology of (TopSpaceNorm V1) #) & TopStruct(# the carrier of (LinearTopSpaceNorm V), the topology of (LinearTopSpaceNorm V) #) = TopStruct(# the carrier of (TopSpaceNorm V), the topology of (TopSpaceNorm V) #) ) by NORMSP_2:def 4;
hence LinearTopSpaceNorm V1 is SubSpace of LinearTopSpaceNorm V by Th1, PRE_TOPC:10; :: thesis: verum