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 ;
assume Z = {x} ; :: thesis: [:Y,(X | Z):],Y are_homeomorphic
then [:(X | Z),Y:],Y are_homeomorphic by Th13;
then consider f being Function of [:(X | Z),Y:],Y such that
A2: f is being_homeomorphism ;
reconsider gf = f * g as Function of [:Y,(X | Z):],Y ;
gf is being_homeomorphism by A2, A1, TOPS_2:57;
hence [:Y,(X | Z):],Y are_homeomorphic ; :: thesis: verum