theorem Th12: :: MESFUN17:12

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