let T be non empty TopSpace; :: thesis:
let a, b be Point of T; :: thesis:
let P be Path of a,b; :: thesis:
assume A1: a,b are_connected ; :: thesis:
defpred S₁[ set , set ] means $2 = P . ($1 `1 );
A2: for x being set st x in [:the carrier of I[01] ,the carrier of I[01] :] holds
ex y being set st
( y in the carrier of T & S₁[x,y] )

let x be set ; :: thesis:
assume x in [:the carrier of I[01] ,the carrier of I[01] :] ; :: thesis:
then x `1 in the carrier of I[01] by MCART_1:10;
hence ex y being set st
( y in the carrier of T & S₁[x,y] ) by FUNCT_2:7; :: thesis:

end;

consider f being Function of [:the carrier of I[01] ,the carrier of I[01] :],the carrier of T such that
A3: for x being set st x in [:the carrier of I[01] ,the carrier of I[01] :] holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
the carrier of [:I[01] ,I[01] :] = [:the carrier of I[01] ,the carrier of I[01] :] by BORSUK_1:def 5;
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 ;
take f ; :: according to BORSUK_2:def 7 :: thesis:
A4: 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

let W be Point of [:I[01] ,I[01] :]; :: thesis:
let G be a_neighborhood of f . W; :: thesis:
W in the carrier of [:I[01] ,I[01] :] ;
then A5: W in [:the carrier of I[01] ,the carrier of I[01] :] by BORSUK_1:def 5;
then reconsider W1 = W `1 as Point of I[01] by MCART_1:10;
reconsider G' = G as a_neighborhood of P . W1 by A3, A5;
P is continuous by A1, Def2;
then consider H being a_neighborhood of W1 such that
A6: P .: H c= G' by BORSUK_1:def 3;
A7: W1 in Int H by CONNSP_2:def 1;
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:118;
then reconsider HH = [:H,the carrier of I[01] :] as Subset of [:I[01] ,I[01] :] by BORSUK_1:def 5;
the carrier of I[01] c= the carrier of I[01] ;
then reconsider AI = the carrier of I[01] as Subset of I[01] ;
A8: AI = [#] I[01] ;
A9: Int HH = [:(Int H),(Int AI):] by BORSUK_1:47;
A10: ex x, y being set st [x,y] = W by A5, RELAT_1:def 1;
Int AI = the carrier of I[01] by A8, TOPS_1:43;
then W `2 in Int AI by A5, MCART_1:10;
then W in Int HH by A7, A9, A10, MCART_1:11;
then reconsider HH = HH as a_neighborhood of W by CONNSP_2:def 1;
take HH ; :: thesis:
f .: HH c= G

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in f .: HH ; :: thesis:
then consider b being set such that
A11: ( b in dom f & b in HH & a = f . b ) by FUNCT_1:def 12;
A12: dom f = [:the carrier of I[01] ,the carrier of I[01] :] by FUNCT_2:def 1;
reconsider b = b as Point of [:I[01] ,I[01] :] by A11;
dom P = the carrier of I[01] by FUNCT_2:def 1;
then A13: ( b `1 in H & b `1 in dom P ) by A11, A12, MCART_1:10;
f . b = P . (b `1 ) by A3, A11, A12;
then f . b in P .: H by A13, FUNCT_1:def 12;
hence a in G by A6, A11; :: thesis:

end;

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

end;

A14: for s being Point of I[01] holds
( f . s,0 = P . s & f . s,1 = P . s )

let s be Point of I[01] ; :: thesis:
reconsider s0 = [s,0 ], s1 = [s,1] as set ;
( s in the carrier of I[01] & 0 in the carrier of I[01] & 1 in the carrier of I[01] ) by Lm1;
then ( s0 in [:the carrier of I[01] ,the carrier of I[01] :] & s1 in [:the carrier of I[01] ,the carrier of I[01] :] ) by ZFMISC_1:106;
then ( S₁[s0,f . s0] & S₁[s1,f . s1] ) by A3;
hence ( f . s,0 = P . s & f . s,1 = P . s ) by MCART_1:7; :: thesis:

end;

for t being Point of I[01] holds
( f . 0 ,t = a & f . 1,t = b )

let t be Point of I[01] ; :: thesis:
set t0 = [0 ,t];
set t1 = [1,t];
A15: ( P . 0 = a & P . 1 = b ) by A1, Def2;
( t in the carrier of I[01] & 0 in the carrier of I[01] & 1 in the carrier of I[01] ) by Lm1;
then ( [0 ,t] in [:the carrier of I[01] ,the carrier of I[01] :] & [1,t] in [:the carrier of I[01] ,the carrier of I[01] :] ) by ZFMISC_1:106;
then ( f . [0 ,t] = P . ([0 ,t] `1 ) & f . [1,t] = P . ([1,t] `1 ) ) by A3;
hence ( f . 0 ,t = a & f . 1,t = b ) by A15, MCART_1:7; :: thesis:

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 A4, A14, BORSUK_1:def 3; :: thesis: