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

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