let T be non empty TopSpace; :: thesis: for t being Point of T
for n being Nat
for S being non empty Subset of T st n >= 2 & S = ([#] T) \ {t} & TOP-REAL n,T are_homeomorphic holds
T | S is pathwise_connected
let t be Point of T; :: thesis: for n being Nat
for S being non empty Subset of T st n >= 2 & S = ([#] T) \ {t} & TOP-REAL n,T are_homeomorphic holds
T | S is pathwise_connected
let n be Nat; :: thesis: for S being non empty Subset of T st n >= 2 & S = ([#] T) \ {t} & TOP-REAL n,T are_homeomorphic holds
T | S is pathwise_connected
let S be non empty Subset of T; :: thesis: ( n >= 2 & S = ([#] T) \ {t} & TOP-REAL n,T are_homeomorphic implies T | S is pathwise_connected )
assume A1: ( n >= 2 & S = ([#] T) \ {t} & TOP-REAL n,T are_homeomorphic ) ; :: thesis: T | S is pathwise_connected
then consider f being Function of T,(TOP-REAL n) such that
A2: f is being_homeomorphism by T_0TOPSP:def 1;
reconsider p = f . t as Point of (TOP-REAL n) ;
reconsider SN = ([#] (TOP-REAL n)) \ {p} as non empty Subset of (TOP-REAL n) by A1, RAMSEY_1:4;
A3: (TOP-REAL n) | SN is pathwise_connected by A1, Th9;
A4: ( dom f = [#] T & rng f = [#] (TOP-REAL n) ) by A2, TOPS_2:58;
then A5: f " ([#] (TOP-REAL n)) = [#] T by RELAT_1:134;
consider x being object such that
A6: f " {p} = {x} by A4, A2, FUNCT_1:74;
A7: x in f " {p} by A6, TARSKI:def 1;
then ( x in dom f & f . x in {p} ) by FUNCT_1:def 7;
then p = f . x by TARSKI:def 1;
then x = t by A2, A7, A4, FUNCT_1:def 4;
then A8: f " SN = S by A1, A5, A6, FUNCT_1:69;
A9: dom (SN |` f) = f " SN by MFOLD_2:1
.= [#] (T | (f " SN)) by PRE_TOPC:def 5 ;
rng (SN |` f) c= SN ;
then rng (SN |` f) c= [#] ((TOP-REAL n) | SN) by PRE_TOPC:def 5;
then reconsider g = SN |` f as Function of (T | (f " SN)),((TOP-REAL n) | SN) by A9, FUNCT_2:2;
g is being_homeomorphism by A2, MFOLD_2:4;
then (TOP-REAL n) | SN,T | S are_homeomorphic by A8, T_0TOPSP:def 1;
hence T | S is pathwise_connected by A3, TOPALG_3:9; :: thesis: verum