reconsider TP = the topology of (TopSpaceNorm X) as Subset-Family of X ;
take
RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #)
; ( the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the carrier of X & 0. RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = 0. X & the addF of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the addF of X & the Mult of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the Mult of X & the topology of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the topology of (TopSpaceNorm X) )
thus
( the carrier of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the carrier of X & 0. RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = 0. X & the addF of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the addF of X & the Mult of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the Mult of X & the topology of RLTopStruct(# the carrier of X,(0. X), the addF of X, the Mult of X,TP #) = the topology of (TopSpaceNorm X) )
; verum