let X, Y be non empty TopSpace; :: thesis: 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 being_homeomorphism
let x be Point of X; :: thesis: for f being Function of [:Y,(X | {x}):],Y st f = pr1 the carrier of Y,{x} holds
f is being_homeomorphism
let f be Function of [:Y,(X | {x}):],Y; :: thesis: ( f = pr1 the carrier of Y,{x} implies f is being_homeomorphism )
set Z = {x};
assume A1: f = pr1 the carrier of Y,{x} ; :: thesis: f is being_homeomorphism
A2: the carrier of (X | {x}) = {x} by PRE_TOPC:29;
thus dom f = [#] [:Y,(X | {x}):] by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng f = [#] Y & f is one-to-one & f is continuous & f " is continuous )
thus rng f = [#] Y by A1, FUNCT_3:60; :: thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus f is one-to-one by A1, Th6; :: thesis: ( f is continuous & f " is continuous )
thus f is continuous by A1, A2, YELLOW12:39; :: thesis: f " is continuous
reconsider Z = {x} as non empty Subset of X ;
reconsider idZ = Y --> x as continuous Function of Y,(X | Z) by Th2;
reconsider KA = <:(id Y),idZ:> as continuous Function of Y,[:Y,(X | Z):] by YELLOW12:41;
KA = f " by A1, Th8;
hence f " is continuous ; :: thesis: verum