theorem Th9: :: MESFUN17:9

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