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, the carrier of I:] 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, the carrier of I:] implies ex y being object st
( y in the carrier of T & S1[x,y] ) )

assume x in [: the carrier of I, the carrier of I:] ; :: thesis: ex y being object st
( y in the carrier of T & S1[x,y] )

then x `1 in the carrier of I 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, the carrier of I:], the carrier of T such that
A2: for x being object st x in [: the carrier of I, the carrier of I:] holds
S1[x,f . x] from the carrier of = [: the carrier of I, the carrier of I:] by BORSUK_1:def 2;
then reconsider f = f as Function of the carrier of , the carrier of T ;
reconsider f = f as Function of ,T ;
assume A3: a,b are_connected ; :: thesis:
A4: for t being Point of I holds
( f . (0,t) = a & f . (1,t) = b )
proof
let t be Point of I; :: thesis: ( f . (0,t) = a & f . (1,t) = b )
set t0 = [0,t];
set t1 = [1,t];
0 in the carrier of I by Lm1;
then [0,t] in [: the carrier of I, the carrier of I:] by ZFMISC_1:87;
then A5: f . [0,t] = P . ([0,t] `1) by A2;
1 in the carrier of I by Lm1;
then [1,t] in [: the carrier of I, the carrier of I:] by ZFMISC_1:87;
then A6: f . [1,t] = P . ([1,t] `1) by A2;
( P . 0 = a & P . 1 = b ) by ;
hence ( f . (0,t) = a & f . (1,t) = b ) by A5, A6; :: thesis: verum
end;
A7: for W being Point of
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 ; :: 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 ;
then A8: W in [: the carrier of I, the carrier of I:] by BORSUK_1:def 2;
then reconsider W1 = W `1 as Point of I by MCART_1:10;
A9: ex x, y being object st [x,y] = W by ;
reconsider G9 = G as a_neighborhood of P . W1 by A2, A8;
the carrier of I c= the carrier of I ;
then reconsider AI = the carrier of I as Subset of I ;
AI = [#] I ;
then Int AI = the carrier of I by TOPS_1:15;
then A10: W `2 in Int AI by ;
P is continuous by ;
then consider H being a_neighborhood of W1 such that
A11: P .: H c= G9 ;
set HH = [:H, the carrier of I:];
[:H, the carrier of I:] c= [: the carrier of I, the carrier of I:] by ZFMISC_1:95;
then reconsider HH = [:H, the carrier of I:] as Subset of by BORSUK_1:def 2;
( W1 in Int H & Int HH = [:(Int H),(Int AI):] ) by ;
then W in Int HH by ;
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 by A12;
A15: ( dom P = the carrier of I & b `1 in H ) by ;
dom f = [: the carrier of I, the carrier of I:] by FUNCT_2:def 1;
then f . b = P . (b `1) by ;
then f . b in P .: H by ;
hence a in G by ; :: 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 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 holds
( f . (s,0) = P . s & f . (s,1) = P . s )
proof
let s be Point of I; :: 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 by Lm1;
then s1 in [: the carrier of I, the carrier of I:] by ZFMISC_1:87;
then A16: S1[s1,f . s1] by A2;
0 in the carrier of I by Lm1;
then s0 in [: the carrier of I, the carrier of I:] 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 holds
( f . (t,0) = P . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) ) by A7, A4; :: thesis: verum