let T be non empty TopSpace; :: thesis:
let a, b be Point of T; :: thesis:
let P be Path of a,b; :: thesis:
let Q be constant Path of a,a; :: thesis:
assume A1: a,b are_connected ; :: thesis:
A2: - P is continuous by A1, BORSUK_2:def 2;
set S = [:I[01] ,I[01] :];
set S1 = [:I[01] ,I[01] :] | IAA ;
set S2 = [:I[01] ,I[01] :] | IBB ;
set S3 = [:I[01] ,I[01] :] | ICC ;
reconsider e1 = pr1 the carrier of I[01] ,the carrier of I[01] as continuous Function of [:I[01] ,I[01] :],I[01] by YELLOW12:39;
reconsider e2 = pr2 the carrier of I[01] ,the carrier of I[01] as continuous Function of [:I[01] ,I[01] :],I[01] by YELLOW12:40;
A3: a,a are_connected ;
then reconsider PP = P + (- P) as continuous Path of a,a by BORSUK_2:def 2;
set ff = PP * e1;
reconsider f = (PP * e1) | IAA as Function of ([:I[01] ,I[01] :] | IAA ),T by PRE_TOPC:30;
reconsider f = f as continuous Function of ([:I[01] ,I[01] :] | IAA ),T by TOPMETR:10;
A4: for x being Point of ([:I[01] ,I[01] :] | IAA ) holds f . x = P . (2 * (x `1 ))

proof

let x be Point of ([:I[01] ,I[01] :] | IAA ); :: thesis:
x in the carrier of ([:I[01] ,I[01] :] | IAA ) ;
then A5: x in IAA by PRE_TOPC:29;
then A6: x in the carrier of [:I[01] ,I[01] :] ;
then A7: x in [:the carrier of I[01] ,the carrier of I[01] :] by BORSUK_1:def 5;
then A8: x = [(x `1 ),(x `2 )] by MCART_1:23;
then A9: ( x `1 in the carrier of I[01] & x `2 in the carrier of I[01] ) by A7, ZFMISC_1:106;
then A10: e1 . (x `1 ),(x `2 ) = x `1 by FUNCT_3:def 5;
A11: x in dom e1 by A6, FUNCT_2:def 1;
A12: x `1 <= 1 / 2 by A5, Th67;
f . x = (PP * e1) . x by A5, FUNCT_1:72
.= (P + (- P)) . (e1 . x) by A11, FUNCT_1:23
.= P . (2 * (x `1 )) by A1, A8, A9, A10, A12, BORSUK_2:def 5 ;
hence f . x = P . (2 * (x `1 )) ; :: thesis:

end;

set gg = (- P) * e2;
reconsider gg = (- P) * e2 as continuous Function of [:I[01] ,I[01] :],T by A2;
reconsider g = gg | IBB as Function of ([:I[01] ,I[01] :] | IBB ),T by PRE_TOPC:30;
reconsider g = g as continuous Function of ([:I[01] ,I[01] :] | IBB ),T by TOPMETR:10;
A13: for x being Point of ([:I[01] ,I[01] :] | IBB ) holds g . x = P . (1 - (x `2 ))

proof

let x be Point of ([:I[01] ,I[01] :] | IBB ); :: thesis:
x in the carrier of ([:I[01] ,I[01] :] | IBB ) ;
then A14: x in IBB by PRE_TOPC:29;
then A15: x in the carrier of [:I[01] ,I[01] :] ;
then A16: x in [:the carrier of I[01] ,the carrier of I[01] :] by BORSUK_1:def 5;
then A17: x = [(x `1 ),(x `2 )] by MCART_1:23;
then A18: ( x `1 in the carrier of I[01] & x `2 in the carrier of I[01] ) by A16, ZFMISC_1:106;
then A19: e2 . (x `1 ),(x `2 ) = x `2 by FUNCT_3:def 6;
A20: x in dom e2 by A15, FUNCT_2:def 1;
g . x = gg . x by A14, FUNCT_1:72
.= (- P) . (e2 . x) by A20, FUNCT_1:23
.= P . (1 - (x `2 )) by A1, A17, A18, A19, BORSUK_2:def 6 ;
hence g . x = P . (1 - (x `2 )) ; :: thesis:

end;

set hh = PP * e1;
reconsider h = (PP * e1) | ICC as Function of ([:I[01] ,I[01] :] | ICC ),T by PRE_TOPC:30;
reconsider h = h as continuous Function of ([:I[01] ,I[01] :] | ICC ),T by TOPMETR:10;
A21: for x being Point of ([:I[01] ,I[01] :] | ICC ) holds h . x = (- P) . ((2 * (x `1 )) - 1)

proof

let x be Point of ([:I[01] ,I[01] :] | ICC ); :: thesis:
x in the carrier of ([:I[01] ,I[01] :] | ICC ) ;
then A22: x in ICC by PRE_TOPC:29;
then A23: x in the carrier of [:I[01] ,I[01] :] ;
then A24: x in [:the carrier of I[01] ,the carrier of I[01] :] by BORSUK_1:def 5;
then A25: x = [(x `1 ),(x `2 )] by MCART_1:23;
then A26: ( x `1 in the carrier of I[01] & x `2 in the carrier of I[01] ) by A24, ZFMISC_1:106;
then A27: e1 . (x `1 ),(x `2 ) = x `1 by FUNCT_3:def 5;
A28: x in dom e1 by A23, FUNCT_2:def 1;
A29: x `1 >= 1 / 2 by A22, Th68;
h . x = (PP * e1) . x by A22, FUNCT_1:72
.= (P + (- P)) . (e1 . x) by A28, FUNCT_1:23
.= (- P) . ((2 * (x `1 )) - 1) by A1, A25, A26, A27, A29, BORSUK_2:def 5 ;
hence h . x = (- P) . ((2 * (x `1 )) - 1) ; :: thesis:

end;

set S12 = [:I[01] ,I[01] :] | (IAA \/ IBB );
reconsider S12 = [:I[01] ,I[01] :] | (IAA \/ IBB ) as non empty SubSpace of [:I[01] ,I[01] :] ;
A30: the carrier of S12 = IAA \/ IBB by PRE_TOPC:29;
A31: [#] ([:I[01] ,I[01] :] | IAA ) = IAA by PRE_TOPC:def 10;
A32: [#] ([:I[01] ,I[01] :] | IBB ) = IBB by PRE_TOPC:def 10;
then reconsider s1 = [#] ([:I[01] ,I[01] :] | IAA ), s2 = [#] ([:I[01] ,I[01] :] | IBB ) as Subset of S12 by A30, A31, XBOOLE_1:7;
A33: ([#] ([:I[01] ,I[01] :] | IAA )) \/ ([#] ([:I[01] ,I[01] :] | IBB )) = [#] S12 by A30, A32, PRE_TOPC:def 10;
A34: for p being set st p in ([#] ([:I[01] ,I[01] :] | IAA )) /\ ([#] ([:I[01] ,I[01] :] | IBB )) holds
f . p = g . p

proof

let p be set ; :: thesis:
assume p in ([#] ([:I[01] ,I[01] :] | IAA )) /\ ([#] ([:I[01] ,I[01] :] | IBB )) ; :: thesis:
then p in ([#] ([:I[01] ,I[01] :] | IAA )) /\ IBB by PRE_TOPC:def 10;
then A35: p in IAA /\ IBB by PRE_TOPC:def 10;
then consider r being Point of [:I[01] ,I[01] :] such that
A36: ( r = p & r `2 = 1 - (2 * (r `1 )) ) by Th65;
A37: ( p in IAA & p in IBB ) by A35, XBOOLE_0:def 4;
then reconsider pp = p as Point of ([:I[01] ,I[01] :] | IAA ) by PRE_TOPC:29;
A38: 2 * (r `1 ) = 1 - (r `2 ) by A36;
A39: pp is Point of ([:I[01] ,I[01] :] | IBB ) by A37, PRE_TOPC:29;
f . p = P . (2 * (pp `1 )) by A4
.= g . p by A13, A36, A38, A39 ;
hence f . p = g . p ; :: thesis:

end;

A40: [:I[01] ,I[01] :] | IAA is SubSpace of S12 by TOPMETR:29, XBOOLE_1:7;
A41: [:I[01] ,I[01] :] | IBB is SubSpace of S12 by TOPMETR:29, XBOOLE_1:7;
A42: s1 is closed by A31, TOPS_2:34;
s2 is closed by A32, TOPS_2:34;
then consider fg being Function of S12,T such that
A43: ( fg = f +* g & fg is continuous ) by A33, A34, A40, A41, A42, JGRAPH_2:9;
A44: [#] ([:I[01] ,I[01] :] | ICC ) = ICC by PRE_TOPC:def 10;
reconsider s12 = [#] S12, s3 = [#] ([:I[01] ,I[01] :] | ICC ) as Subset of [:I[01] ,I[01] :] by PRE_TOPC:def 10;
A45: ([#] S12) \/ ([#] ([:I[01] ,I[01] :] | ICC )) = (IAA \/ IBB ) \/ ICC by A30, PRE_TOPC:def 10
.= [#] [:I[01] ,I[01] :] by Th64, BORSUK_1:83, BORSUK_1:def 5 ;
A46: for p being set st p in ([#] S12) /\ ([#] ([:I[01] ,I[01] :] | ICC )) holds
fg . p = h . p

proof

let p be set ; :: thesis:
assume p in ([#] S12) /\ ([#] ([:I[01] ,I[01] :] | ICC )) ; :: thesis:
then A47: p in {[(1 / 2),0 ]} \/ (IBB /\ ICC ) by A30, A44, Th80, XBOOLE_1:23;
[(1 / 2),0 ] in IBB /\ ICC by Th74, Th75, XBOOLE_0:def 4;
then {[(1 / 2),0 ]} c= IBB /\ ICC by ZFMISC_1:37;
then A48: p in IBB /\ ICC by A47, XBOOLE_1:12;
then consider q being Point of [:I[01] ,I[01] :] such that
A49: ( q = p & q `2 = (2 * (q `1 )) - 1 ) by Th66;
A50: ( p in IBB & p in ICC ) by A48, XBOOLE_0:def 4;
then reconsider pp = p as Point of ([:I[01] ,I[01] :] | ICC ) by PRE_TOPC:29;
A51: pp is Point of ([:I[01] ,I[01] :] | IBB ) by A50, PRE_TOPC:29;
A52: (2 * (pp `1 )) - 1 is Point of I[01] by A49, Th31;
p in the carrier of ([:I[01] ,I[01] :] | IBB ) by A50, PRE_TOPC:29;
then p in dom g by FUNCT_2:def 1;
then fg . p = g . p by A43, FUNCT_4:14
.= P . (1 - (pp `2 )) by A13, A51
.= (- P) . ((2 * (pp `1 )) - 1) by A1, A49, A52, BORSUK_2:def 6
.= h . p by A21 ;
hence fg . p = h . p ; :: thesis:

end;

A53: s12 is closed by A30, TOPS_1:36;
s3 = ICC by PRE_TOPC:def 10;
then consider H being Function of [:I[01] ,I[01] :],T such that
A54: ( H = fg +* h & H is continuous ) by A43, A45, A46, A53, JGRAPH_2:9;
A55: for s being Point of I[01] holds
( H . s,0 = (P + (- P)) . s & H . s,1 = Q . s )

proof

let s be Point of I[01] ; :: thesis:
thus H . s,0 = (P + (- P)) . s :: thesis:

proof

A56: [s,0 ] `1 = s by MCART_1:7;

per cases by XXREAL_0:1;

suppose A57: s < 1 / 2 ; :: thesis:

then A58: [s,0 ] in IAA by Th78;
not [s,0 ] in ICC by A57, Th79;
then not [s,0 ] in the carrier of ([:I[01] ,I[01] :] | ICC ) by PRE_TOPC:29;
then A59: not [s,0 ] in dom h ;
A60: [s,0 ] in the carrier of ([:I[01] ,I[01] :] | IAA ) by A58, PRE_TOPC:29;
not [s,0 ] in IBB by A57, Th79;
then not [s,0 ] in the carrier of ([:I[01] ,I[01] :] | IBB ) by PRE_TOPC:29;
then A61: not [s,0 ] in dom g ;
H . [s,0 ] = fg . [s,0 ] by A54, A59, FUNCT_4:12
.= f . [s,0 ] by A43, A61, FUNCT_4:12
.= P . (2 * s) by A4, A56, A60
.= (P + (- P)) . s by A1, A57, BORSUK_2:def 5 ;
hence H . s,0 = (P + (- P)) . s ; :: thesis:

end;

suppose A62: s = 1 / 2 ; :: thesis:

then A63: [s,0 ] in the carrier of ([:I[01] ,I[01] :] | ICC ) by Th74, PRE_TOPC:29;
then [s,0 ] in dom h by FUNCT_2:def 1;
then H . [s,0 ] = h . [s,0 ] by A54, FUNCT_4:14
.= (- P) . ((2 * s) - 1) by A21, A56, A63
.= b by A1, A62, BORSUK_2:def 2
.= P . (2 * (1 / 2)) by A1, BORSUK_2:def 2
.= (P + (- P)) . s by A1, A62, BORSUK_2:def 5 ;
hence H . s,0 = (P + (- P)) . s ; :: thesis:

end;

suppose A64: s > 1 / 2 ; :: thesis:

then [s,0 ] in ICC by Th77;
then A65: [s,0 ] in the carrier of ([:I[01] ,I[01] :] | ICC ) by PRE_TOPC:29;
then [s,0 ] in dom h by FUNCT_2:def 1;
then H . [s,0 ] = h . [s,0 ] by A54, FUNCT_4:14
.= (- P) . ((2 * s) - 1) by A21, A56, A65
.= (P + (- P)) . s by A1, A64, BORSUK_2:def 5 ;
hence H . s,0 = (P + (- P)) . s ; :: thesis:

end;

thus H . s,1 = Q . s :: thesis:

proof

A66: ( [s,1] `1 = s & [s,1] `2 = 1 ) by MCART_1:7;
dom Q = the carrier of I[01] by FUNCT_2:def 1;
then A67: ( 0 in dom Q & s in dom Q ) by BORSUK_1:86;

per cases ;

suppose s <> 1 ; :: thesis:

then not [s,1] in ICC by Th71;
then not [s,1] in the carrier of ([:I[01] ,I[01] :] | ICC ) by PRE_TOPC:29;
then A68: not [s,1] in dom h ;
[s,1] in IBB by Th73;
then A69: [s,1] in the carrier of ([:I[01] ,I[01] :] | IBB ) by PRE_TOPC:29;
then A70: [s,1] in dom g by FUNCT_2:def 1;
H . [s,1] = fg . [s,1] by A54, A68, FUNCT_4:12
.= g . [s,1] by A43, A70, FUNCT_4:14
.= P . (1 - 1) by A13, A66, A69
.= a by A1, BORSUK_2:def 2
.= Q . 0 by A3, BORSUK_2:def 2
.= Q . s by A67, FUNCT_1:def 16 ;
hence H . s,1 = Q . s ; :: thesis:

end;

suppose A71: s = 1 ; :: thesis:

then A72: [s,1] in the carrier of ([:I[01] ,I[01] :] | ICC ) by Th74, PRE_TOPC:29;
then [s,1] in dom h by FUNCT_2:def 1;
then H . [s,1] = h . [s,1] by A54, FUNCT_4:14
.= (- P) . ((2 * s) - 1) by A21, A66, A72
.= a by A1, A71, BORSUK_2:def 2
.= Q . 0 by A3, BORSUK_2:def 2
.= Q . s by A67, FUNCT_1:def 16 ;
hence H . s,1 = Q . s ; :: thesis:

end;

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

proof

let t be Point of I[01] ; :: thesis:
thus H . 0 ,t = a :: thesis:

proof

0 in the carrier of I[01] by BORSUK_1:86;
then reconsider x = [0 ,t] as Point of [:I[01] ,I[01] :] by Lm1;
x in IAA by Th69;
then A73: x is Point of ([:I[01] ,I[01] :] | IAA ) by PRE_TOPC:29;
A74: ( x `1 = 0 & x `2 = t ) by MCART_1:7;
then not x in ICC by Th68;
then not x in the carrier of ([:I[01] ,I[01] :] | ICC ) by PRE_TOPC:29;
then A75: not [0 ,t] in dom h ;

per cases ;

suppose t <> 1 ; :: thesis:

then not x in IBB by Th70;
then not x in the carrier of ([:I[01] ,I[01] :] | IBB ) by PRE_TOPC:29;
then not x in dom g ;
then fg . [0 ,t] = f . [0 ,t] by A43, FUNCT_4:12
.= P . (2 * (x `1 )) by A4, A73
.= a by A1, A74, BORSUK_2:def 2 ;
hence H . 0 ,t = a by A54, A75, FUNCT_4:12; :: thesis:

end;

suppose A76: t = 1 ; :: thesis:

then A77: x in the carrier of ([:I[01] ,I[01] :] | IBB ) by Th72, PRE_TOPC:29;
then x in dom g by FUNCT_2:def 1;
then fg . [0 ,t] = g . [0 ,1] by A43, A76, FUNCT_4:14
.= P . (1 - (x `2 )) by A13, A76, A77
.= a by A1, A74, A76, BORSUK_2:def 2 ;
hence H . 0 ,t = a by A54, A75, FUNCT_4:12; :: thesis:

end;

thus H . 1,t = a :: thesis:

proof

1 in the carrier of I[01] by BORSUK_1:86;
then reconsider x = [1,t] as Point of [:I[01] ,I[01] :] by Lm1;
A78: x in ICC by Th76;
A79: ( x `1 = 1 & x `2 = t ) by MCART_1:7;
A80: x in the carrier of ([:I[01] ,I[01] :] | ICC ) by A78, PRE_TOPC:29;
then A81: [1,t] in dom h by FUNCT_2:def 1;
h . [1,t] = (- P) . ((2 * (x `1 )) - 1) by A21, A80
.= a by A1, A79, BORSUK_2:def 2 ;
hence H . 1,t = a by A54, A81, FUNCT_4:14; :: thesis:

end;

hence P + (- P),Q are_homotopic by A54, A55, BORSUK_2:def 7; :: thesis: