let M, N be non empty TopSpace; :: thesis:
let p be Point of M; :: thesis:
let U be a_neighborhood of p; :: thesis:
let B be open Subset of N; :: thesis:
assume A0: U,B are_homeomorphic ; :: thesis:
then A1: M | U,N | B are_homeomorphic by METRIZTS:def 1;
consider f being Function of (M | U),(N | B) such that
A2: f is being_homeomorphism by T_0TOPSP:def 1, A0, METRIZTS:def 1;
consider V being Subset of M such that
A3: ( V is open & V c= U & p in V ) by CONNSP_2:6;
V c= [#] (M | U) by A3, PRE_TOPC:def 5;
then reconsider V1 = V as Subset of (M | U) ;
reconsider M1 = M | U as non empty TopStruct by A3;
reconsider N1 = N | B as non empty TopStruct by A3, A1, YELLOW14:18;
reconsider f1 = f as Function of M1,N1 ;
rng f c= [#] (N | B) ;
then A4: rng f c= B by PRE_TOPC:def 5;
A5: (M | U) | V1,(N | B) | (f .: V1) are_homeomorphic by METRIZTS:def 1, A2, METRIZTS:3;
reconsider V = V as open Subset of M by A3;
B = the carrier of (N | B) by PRE_TOPC:8;
then reconsider N1 = N | B as open SubSpace of N by TSEP_1:16;
B c= the carrier of N ;
then [#] (N | B) c= the carrier of N by PRE_TOPC:def 5;
then reconsider S = f .: V1 as Subset of N by XBOOLE_1:1;
reconsider S1 = f .: V1 as Subset of N1 ;
A6: for P being Subset of M1 holds
( P is open iff f1 .: P is open ) by A2, TOPGRP_1:25;
A7: V in the topology of M by PRE_TOPC:def 2;
V1 = V /\ ([#] M1) by XBOOLE_1:28;
then V1 in the topology of M1 by A7, PRE_TOPC:def 4;
then S1 is open by A6, PRE_TOPC:def 2;
then reconsider S = S as open Subset of N by TSEP_1:17;
take V ; :: thesis:
take S ; :: thesis:
thus ( V c= U & p in V ) by A3; :: thesis:
A8: (M | U) | V1 = M | V by A3, PRE_TOPC:7;
f .: U c= rng f by RELAT_1:111;
then A9: f .: U c= B by A4;
f .: V c= f .: U by A3, RELAT_1:123;
then (N | B) | (f .: V1) = N | S by A9, PRE_TOPC:7, XBOOLE_1:1;
hence V,S are_homeomorphic by A5, A8, METRIZTS:def 1; :: thesis: