let X, Y be non empty TopSpace; for x being Point of X holds [:(X | {x}),Y:],Y are_homeomorphic
let x be Point of X; [:(X | {x}),Y:],Y are_homeomorphic
set Z = {x};
the carrier of [:(X | {x}),Y:] =
[: the carrier of (X | {x}), the carrier of Y:]
by BORSUK_1:def 2
.=
[:{x}, the carrier of Y:]
by PRE_TOPC:8
;
then reconsider f = pr2 ({x}, the carrier of Y) as Function of [:(X | {x}),Y:],Y ;
take
f
; T_0TOPSP:def 1 f is being_homeomorphism
thus
f is being_homeomorphism
by Th9; verum