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
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:44; :: thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus f is one-to-one by A1, Th4; :: thesis: ( f is continuous & f " is continuous )
the carrier of (X | {x}) = {x} by PRE_TOPC:8;
hence f is continuous by A1, 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, Th6;
hence f " is continuous ; :: thesis: verum