theorem Th20: :: MESFUN17:20

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