theorem Th4: :: BORSUK_3:4

for X, Y being non empty TopSpace
for x being Point of X
for f being Function of [:Y,(X | {x}):],Y st f = pr1 ( the carrier of Y,{x}) holds
f is one-to-one