theorem Th19: :: MESFUN16:19
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st f = g holds
||.f.|| = |.g.|