let T be non empty TopSpace; :: thesis: for a, b being Point of T

for P being Path of a,b st a,b are_connected holds

P,P are_homotopic

let a, b be Point of T; :: thesis: for P being Path of a,b st a,b are_connected holds

P,P are_homotopic

let P be Path of a,b; :: thesis: ( a,b are_connected implies P,P are_homotopic )

defpred S_{1}[ object , object ] means $2 = P . ($1 `1);

A1: for x being object st x in [: the carrier of I[01], the carrier of I[01]:] holds

ex y being object st

( y in the carrier of T & S_{1}[x,y] )

A2: for x being object st x in [: the carrier of I[01], the carrier of I[01]:] holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A1);

the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;

then reconsider f = f as Function of the carrier of [:I[01],I[01]:], the carrier of T ;

reconsider f = f as Function of [:I[01],I[01]:],T ;

assume A3: a,b are_connected ; :: thesis: P,P are_homotopic

A4: for t being Point of I[01] holds

( f . (0,t) = a & f . (1,t) = b )

for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G

( f . (t,0) = P . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) )

for s being Point of I[01] holds

( f . (s,0) = P . s & f . (s,1) = P . s )

( f . (t,0) = P . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) ) by A7, A4; :: thesis: verum

for P being Path of a,b st a,b are_connected holds

P,P are_homotopic

let a, b be Point of T; :: thesis: for P being Path of a,b st a,b are_connected holds

P,P are_homotopic

let P be Path of a,b; :: thesis: ( a,b are_connected implies P,P are_homotopic )

defpred S

A1: for x being object st x in [: the carrier of I[01], the carrier of I[01]:] holds

ex y being object st

( y in the carrier of T & S

proof

consider f being Function of [: the carrier of I[01], the carrier of I[01]:], the carrier of T such that
let x be object ; :: thesis: ( x in [: the carrier of I[01], the carrier of I[01]:] implies ex y being object st

( y in the carrier of T & S_{1}[x,y] ) )

assume x in [: the carrier of I[01], the carrier of I[01]:] ; :: thesis: ex y being object st

( y in the carrier of T & S_{1}[x,y] )

then x `1 in the carrier of I[01] by MCART_1:10;

hence ex y being object st

( y in the carrier of T & S_{1}[x,y] )
by FUNCT_2:5; :: thesis: verum

end;( y in the carrier of T & S

assume x in [: the carrier of I[01], the carrier of I[01]:] ; :: thesis: ex y being object st

( y in the carrier of T & S

then x `1 in the carrier of I[01] by MCART_1:10;

hence ex y being object st

( y in the carrier of T & S

A2: for x being object st x in [: the carrier of I[01], the carrier of I[01]:] holds

S

the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;

then reconsider f = f as Function of the carrier of [:I[01],I[01]:], the carrier of T ;

reconsider f = f as Function of [:I[01],I[01]:],T ;

assume A3: a,b are_connected ; :: thesis: P,P are_homotopic

A4: for t being Point of I[01] holds

( f . (0,t) = a & f . (1,t) = b )

proof

A7:
for W being Point of [:I[01],I[01]:]
let t be Point of I[01]; :: thesis: ( f . (0,t) = a & f . (1,t) = b )

set t0 = [0,t];

set t1 = [1,t];

0 in the carrier of I[01] by Lm1;

then [0,t] in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;

then A5: f . [0,t] = P . ([0,t] `1) by A2;

1 in the carrier of I[01] by Lm1;

then [1,t] in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;

then A6: f . [1,t] = P . ([1,t] `1) by A2;

( P . 0 = a & P . 1 = b ) by A3, Def2;

hence ( f . (0,t) = a & f . (1,t) = b ) by A5, A6; :: thesis: verum

end;set t0 = [0,t];

set t1 = [1,t];

0 in the carrier of I[01] by Lm1;

then [0,t] in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;

then A5: f . [0,t] = P . ([0,t] `1) by A2;

1 in the carrier of I[01] by Lm1;

then [1,t] in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;

then A6: f . [1,t] = P . ([1,t] `1) by A2;

( P . 0 = a & P . 1 = b ) by A3, Def2;

hence ( f . (0,t) = a & f . (1,t) = b ) by A5, A6; :: thesis: verum

for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G

proof

take
f
; :: according to BORSUK_2:def 7 :: thesis: ( f is continuous & ( for t being Point of I[01] holds
let W be Point of [:I[01],I[01]:]; :: thesis: for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G

let G be a_neighborhood of f . W; :: thesis: ex H being a_neighborhood of W st f .: H c= G

W in the carrier of [:I[01],I[01]:] ;

then A8: W in [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;

then reconsider W1 = W `1 as Point of I[01] by MCART_1:10;

A9: ex x, y being object st [x,y] = W by A8, RELAT_1:def 1;

reconsider G9 = G as a_neighborhood of P . W1 by A2, A8;

the carrier of I[01] c= the carrier of I[01] ;

then reconsider AI = the carrier of I[01] as Subset of I[01] ;

AI = [#] I[01] ;

then Int AI = the carrier of I[01] by TOPS_1:15;

then A10: W `2 in Int AI by A8, MCART_1:10;

P is continuous by A3, Def2;

then consider H being a_neighborhood of W1 such that

A11: P .: H c= G9 ;

set HH = [:H, the carrier of I[01]:];

[:H, the carrier of I[01]:] c= [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:95;

then reconsider HH = [:H, the carrier of I[01]:] as Subset of [:I[01],I[01]:] by BORSUK_1:def 2;

( W1 in Int H & Int HH = [:(Int H),(Int AI):] ) by BORSUK_1:7, CONNSP_2:def 1;

then W in Int HH by A9, A10, ZFMISC_1:def 2;

then reconsider HH = HH as a_neighborhood of W by CONNSP_2:def 1;

take HH ; :: thesis: f .: HH c= G

f .: HH c= G

end;let G be a_neighborhood of f . W; :: thesis: ex H being a_neighborhood of W st f .: H c= G

W in the carrier of [:I[01],I[01]:] ;

then A8: W in [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;

then reconsider W1 = W `1 as Point of I[01] by MCART_1:10;

A9: ex x, y being object st [x,y] = W by A8, RELAT_1:def 1;

reconsider G9 = G as a_neighborhood of P . W1 by A2, A8;

the carrier of I[01] c= the carrier of I[01] ;

then reconsider AI = the carrier of I[01] as Subset of I[01] ;

AI = [#] I[01] ;

then Int AI = the carrier of I[01] by TOPS_1:15;

then A10: W `2 in Int AI by A8, MCART_1:10;

P is continuous by A3, Def2;

then consider H being a_neighborhood of W1 such that

A11: P .: H c= G9 ;

set HH = [:H, the carrier of I[01]:];

[:H, the carrier of I[01]:] c= [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:95;

then reconsider HH = [:H, the carrier of I[01]:] as Subset of [:I[01],I[01]:] by BORSUK_1:def 2;

( W1 in Int H & Int HH = [:(Int H),(Int AI):] ) by BORSUK_1:7, CONNSP_2:def 1;

then W in Int HH by A9, A10, ZFMISC_1:def 2;

then reconsider HH = HH as a_neighborhood of W by CONNSP_2:def 1;

take HH ; :: thesis: f .: HH c= G

f .: HH c= G

proof

hence
f .: HH c= G
; :: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in f .: HH or a in G )

assume a in f .: HH ; :: thesis: a in G

then consider b being object such that

A12: b in dom f and

A13: b in HH and

A14: a = f . b by FUNCT_1:def 6;

reconsider b = b as Point of [:I[01],I[01]:] by A12;

A15: ( dom P = the carrier of I[01] & b `1 in H ) by A13, FUNCT_2:def 1, MCART_1:10;

dom f = [: the carrier of I[01], the carrier of I[01]:] by FUNCT_2:def 1;

then f . b = P . (b `1) by A2, A12;

then f . b in P .: H by A15, FUNCT_1:def 6;

hence a in G by A11, A14; :: thesis: verum

end;assume a in f .: HH ; :: thesis: a in G

then consider b being object such that

A12: b in dom f and

A13: b in HH and

A14: a = f . b by FUNCT_1:def 6;

reconsider b = b as Point of [:I[01],I[01]:] by A12;

A15: ( dom P = the carrier of I[01] & b `1 in H ) by A13, FUNCT_2:def 1, MCART_1:10;

dom f = [: the carrier of I[01], the carrier of I[01]:] by FUNCT_2:def 1;

then f . b = P . (b `1) by A2, A12;

then f . b in P .: H by A15, FUNCT_1:def 6;

hence a in G by A11, A14; :: thesis: verum

( f . (t,0) = P . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) )

for s being Point of I[01] holds

( f . (s,0) = P . s & f . (s,1) = P . s )

proof

hence
( f is continuous & ( for t being Point of I[01] holds
let s be Point of I[01]; :: thesis: ( f . (s,0) = P . s & f . (s,1) = P . s )

reconsider s0 = [s,0], s1 = [s,1] as set ;

1 in the carrier of I[01] by Lm1;

then s1 in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;

then A16: S_{1}[s1,f . s1]
by A2;

0 in the carrier of I[01] by Lm1;

then s0 in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;

then S_{1}[s0,f . s0]
by A2;

hence ( f . (s,0) = P . s & f . (s,1) = P . s ) by A16; :: thesis: verum

end;reconsider s0 = [s,0], s1 = [s,1] as set ;

1 in the carrier of I[01] by Lm1;

then s1 in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;

then A16: S

0 in the carrier of I[01] by Lm1;

then s0 in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;

then S

hence ( f . (s,0) = P . s & f . (s,1) = P . s ) by A16; :: thesis: verum

( f . (t,0) = P . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) ) by A7, A4; :: thesis: verum