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