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:
then consider f being Function of T,() such that
A2: f is being_homeomorphism by T_0TOPSP:def 1;
reconsider p = f . t as Point of () ;
reconsider SN = ([#] ()) \ {p} as non empty Subset of () by ;
A3: (TOP-REAL n) | SN is pathwise_connected by ;
A4: ( dom f = [#] T & rng f = [#] () ) by ;
then A5: f " ([#] ()) = [#] T by RELAT_1:134;
consider x being object such that
A6: f " {p} = {x} by ;
A7: x in f " {p} by ;
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 ;
then A8: f " SN = S by ;
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= [#] (() | SN) by PRE_TOPC:def 5;
then reconsider g = SN |` f as Function of (T | (f " SN)),(() | SN) by ;
g is being_homeomorphism by ;
then (TOP-REAL n) | SN,T | S are_homeomorphic by ;
hence T | S is pathwise_connected by ; :: thesis: verum