let X, Y be non empty TopSpace; :: thesis: for x being Point of X
for Z being non empty Subset of X st Z = {x} holds
[:Y,(X | Z):],Y are_homeomorphic
let x be Point of X; :: thesis: for Z being non empty Subset of X st Z = {x} holds
[:Y,(X | Z):],Y are_homeomorphic
let Z be non empty Subset of X; :: thesis: ( Z = {x} implies [:Y,(X | Z):],Y are_homeomorphic )
[:Y,(X | Z):],[:(X | Z),Y:] are_homeomorphic by YELLOW12:44;
then consider g being Function of [:Y,(X | Z):],[:(X | Z),Y:] such that
A1: g is being_homeomorphism by T_0TOPSP:def 1;
assume Z = {x} ; :: thesis: [:Y,(X | Z):],Y are_homeomorphic
then [:(X | Z),Y:],Y are_homeomorphic by Th15;
then consider f being Function of [:(X | Z),Y:],Y such that
A2: f is being_homeomorphism by T_0TOPSP:def 1;
reconsider gf = f * g as Function of [:Y,(X | Z):],Y ;
gf is being_homeomorphism by A2, A1, TOPS_2:71;
hence [:Y,(X | Z):],Y are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum