theorem Th22: :: NEURONS1:22

for RNS being RealNormSpace holds NORMSTR(# the carrier of RNS, the ZeroF of RNS, the addF of RNS, the Mult of RNS, the normF of RNS #) is strict RealNormSpace