let X, Y be non empty TopSpace; :: thesis: for x being Point of X
for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds
f is being_homeomorphism
let x be Point of X; :: thesis: for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds
f is being_homeomorphism
let f be Function of [:(X | {x}),Y:],Y; :: thesis: ( f = pr2 ({x}, the carrier of Y) implies f is being_homeomorphism )
set Z = {x};
assume A1: f = pr2 ({x}, the carrier of Y) ; :: thesis: f is being_homeomorphism
thus dom f = [#] [:(X | {x}),Y:] 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:46; :: thesis: ( f is one-to-one & f is continuous & f " is continuous )
thus f is one-to-one by A1, Th5; :: thesis: ( f is continuous & f " is continuous )
the carrier of (X | {x}) = {x} by PRE_TOPC:8;
hence f is continuous by A1, YELLOW12:40; :: 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 = <:idZ,(id Y):> as continuous Function of Y,[:(X | Z),Y:] by YELLOW12:41;
KA = f " by A1, Th7;
hence f " is continuous ; :: thesis: verum