theorem Th13: :: JORDAN20:13

for P being non empty Subset of (TOP-REAL 2)
for P1 being Subset of ((TOP-REAL 2) | P)
for Q being Subset of I[01]
for f being Function of I[01],((TOP-REAL 2) | P)
for s being Real st s <= 1 & P1 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( 0 <= ss & ss < s & q0 = f . ss ) } & Q = [.0,s.[ holds
f .: Q = P1