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 S1[ 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 & S1[x,y] )
proof
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 & S1[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 & S1[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 & S1[x,y] ) by FUNCT_2:5; :: thesis: verum
end;
consider f being Function of [: the carrier of I[01], the carrier of I[01]:], the carrier of T such that
A2: for x being object st x in [: the carrier of I[01], the carrier of I[01]:] holds
S1[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 )
proof
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;
A7: for W being Point of [:I[01],I[01]:]
for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
proof
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
proof
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;
hence f .: HH c= G ; :: thesis: verum
end;
take f ; :: according to BORSUK_2:def 7 :: thesis: ( f is continuous & ( for t being Point of I[01] holds
( 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
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: S1[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 S1[s0,f . s0] by A2;
hence ( f . (s,0) = P . s & f . (s,1) = P . s ) by A16; :: thesis: verum
end;
hence ( f is continuous & ( for t being Point of I[01] holds
( f . (t,0) = P . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) ) by A7, A4; :: thesis: verum