theorem Th18: :: MESFUN17:18

for z being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pf2 being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real st f is_continuous_on dom f & f = g & Pf2 = ProjPMap2 ((R_EAL g),z) holds
Pf2 is_continuous_on dom Pf2