theorem Th12: :: TOPREAL5:12

for P being non empty Subset of (TOP-REAL 2)
for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds
ex g being Function of I[01],R^1 st
( g is continuous & ( for r being Real
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = g . r ) )