let T be non empty TopSpace; :: thesis:
let b, a be Point of T; :: thesis:
let P be Path of b,a; :: thesis:
let Q be constant Path of a,a; :: thesis:
assume A1: b,a 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: 1 - (x `2 ) in the carrier of I[01] by A18, JORDAN5B:4;
A21: x in dom e2 by A15, FUNCT_2:def 1;
g . x = gg . (x `1 ),(x `2 ) by A14, A17, FUNCT_1:72
.= P . (1 - (1 - (x `2 ))) by A17, A19, A21, FUNCT_1:23
.= (- P) . (1 - (x `2 )) by A1, A20, 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;
A22: 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 A23: x in ICC by PRE_TOPC:29;
then A24: x in the carrier of [:I[01] ,I[01] :] ;
then A25: x in [:the carrier of I[01] ,the carrier of I[01] :] by BORSUK_1:def 5;
then A26: x = [(x `1 ),(x `2 )] by MCART_1:23;
then A27: ( x `1 in the carrier of I[01] & x `2 in the carrier of I[01] ) by A25, ZFMISC_1:106;
then A28: e1 . (x `1 ),(x `2 ) = x `1 by FUNCT_3:def 5;
A29: x in dom e1 by A24, FUNCT_2:def 1;
A30: x `1 >= 1 / 2 by A23, Th68;
h . x = (PP * e1) . x by A23, FUNCT_1:72
.= ((- P) + P) . (e1 . (x `1 ),(x `2 )) by A26, A29, FUNCT_1:23
.= P . ((2 * (x `1 )) - 1) by A1, A27, A28, A30, 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] :] ;
A31: the carrier of S12 = IAA \/ IBB by PRE_TOPC:29;
A32: [#] ([:I[01] ,I[01] :] | IAA ) = IAA by PRE_TOPC:def 10;
A33: [#] ([: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 A31, A32, XBOOLE_1:7;
A34: ([#] ([:I[01] ,I[01] :] | IAA )) \/ ([#] ([:I[01] ,I[01] :] | IBB )) = [#] S12 by A31, A33, PRE_TOPC:def 10;
A35: 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 A36: p in IAA /\ IBB by PRE_TOPC:def 10;
then consider r being Point of [:I[01] ,I[01] :] such that
A37: ( r = p & r `2 = 1 - (2 * (r `1 )) ) by Th65;
A38: ( p in IAA & p in IBB ) by A36, XBOOLE_0:def 4;
then reconsider pp = p as Point of ([:I[01] ,I[01] :] | IAA ) by PRE_TOPC:29;
A39: 2 * (r `1 ) = 1 - (r `2 ) by A37;
A40: pp is Point of ([:I[01] ,I[01] :] | IBB ) by A38, PRE_TOPC:29;
f . p = (- P) . (2 * (pp `1 )) by A4
.= g . p by A13, A37, A39, A40 ;
hence f . p = g . p ; :: thesis:

end;

A41: [:I[01] ,I[01] :] | IAA is SubSpace of S12 by TOPMETR:29, XBOOLE_1:7;
A42: [:I[01] ,I[01] :] | IBB is SubSpace of S12 by TOPMETR:29, XBOOLE_1:7;
A43: s1 is closed by A32, TOPS_2:34;
s2 is closed by A33, TOPS_2:34;
then consider fg being Function of S12,T such that
A44: ( fg = f +* g & fg is continuous ) by A34, A35, A41, A42, A43, JGRAPH_2:9;
A45: [#] ([: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;
A46: ([#] S12) \/ ([#] ([:I[01] ,I[01] :] | ICC )) = [#] [:I[01] ,I[01] :] by A31, A45, Th64, BORSUK_1:83, BORSUK_1:def 5;
A47: 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 A48: p in {[(1 / 2),0 ]} \/ (IBB /\ ICC ) by A31, A45, 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 A49: p in IBB /\ ICC by A48, XBOOLE_1:12;
then consider q being Point of [:I[01] ,I[01] :] such that
A50: ( q = p & q `2 = (2 * (q `1 )) - 1 ) by Th66;
A51: ( p in IBB & p in ICC ) by A49, XBOOLE_0:def 4;
then reconsider pp = p as Point of ([:I[01] ,I[01] :] | ICC ) by PRE_TOPC:29;
A52: pp is Point of ([:I[01] ,I[01] :] | IBB ) by A51, PRE_TOPC:29;
( pp `1 is Point of I[01] & pp `2 is Point of I[01] ) by A50, Th31;
then A53: 1 - (pp `2 ) in the carrier of I[01] by JORDAN5B:4;
p in the carrier of ([:I[01] ,I[01] :] | IBB ) by A51, PRE_TOPC:29;
then p in dom g by FUNCT_2:def 1;
then fg . p = g . p by A44, FUNCT_4:14
.= (- P) . (1 - (pp `2 )) by A13, A52
.= P . (1 - (1 - (pp `2 ))) by A1, A53, BORSUK_2:def 6
.= h . p by A22, A50 ;
hence fg . p = h . p ; :: thesis:

end;

A54: s12 is closed by A31, TOPS_1:36;
s3 = ICC by PRE_TOPC:def 10;
then consider H being Function of [:I[01] ,I[01] :],T such that
A55: ( H = fg +* h & H is continuous ) by A44, A46, A47, A54, JGRAPH_2:9;
A56: 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

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

per cases by XXREAL_0:1;

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

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

end;

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

then A64: [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 A55, FUNCT_4:14
.= P . ((2 * s) - 1) by A22, A57, A64
.= b by A1, A63, BORSUK_2:def 2
.= (- P) . (2 * (1 / 2)) by A1, BORSUK_2:def 2
.= ((- P) + P) . s by A1, A63, BORSUK_2:def 5 ;
hence H . s,0 = ((- P) + P) . s ; :: thesis:

end;

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

then [s,0 ] in ICC by Th77;
then A66: [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 A55, FUNCT_4:14
.= P . ((2 * s) - 1) by A22, A57, A66
.= ((- P) + P) . s by A1, A65, BORSUK_2:def 5 ;
hence H . s,0 = ((- P) + P) . s ; :: thesis:

end;

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

proof

A67: ( [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 A68: ( 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 A69: not [s,1] in dom h ;
[s,1] in IBB by Th73;
then A70: [s,1] in the carrier of ([:I[01] ,I[01] :] | IBB ) by PRE_TOPC:29;
then A71: [s,1] in dom g by FUNCT_2:def 1;
H . [s,1] = fg . [s,1] by A55, A69, FUNCT_4:12
.= g . [s,1] by A44, A71, FUNCT_4:14
.= (- P) . (1 - 1) by A13, A67, A70
.= a by A1, BORSUK_2:def 2
.= Q . 0 by A3, BORSUK_2:def 2
.= Q . s by A68, FUNCT_1:def 16 ;
hence H . s,1 = Q . s ; :: thesis:

end;

suppose A72: s = 1 ; :: thesis:

then A73: [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 A55, FUNCT_4:14
.= P . ((2 * s) - 1) by A22, A67, A73
.= a by A1, A72, BORSUK_2:def 2
.= Q . 0 by A3, BORSUK_2:def 2
.= Q . s by A68, 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 A74: x is Point of ([:I[01] ,I[01] :] | IAA ) by PRE_TOPC:29;
A75: ( 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 A76: 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 A44, FUNCT_4:12
.= (- P) . (2 * (x `1 )) by A4, A74
.= a by A1, A75, BORSUK_2:def 2 ;
hence H . 0 ,t = a by A55, A76, FUNCT_4:12; :: thesis:

end;

suppose A77: t = 1 ; :: thesis:

then A78: 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 A44, A77, FUNCT_4:14
.= (- P) . (1 - (x `2 )) by A13, A77, A78
.= a by A1, A75, A77, BORSUK_2:def 2 ;
hence H . 0 ,t = a by A55, A76, 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;
A79: x in ICC by Th76;
A80: ( x `1 = 1 & x `2 = t ) by MCART_1:7;
A81: x in the carrier of ([:I[01] ,I[01] :] | ICC ) by A79, PRE_TOPC:29;
then A82: [1,t] in dom h by FUNCT_2:def 1;
h . [1,t] = P . ((2 * (x `1 )) - 1) by A22, A81
.= a by A1, A80, BORSUK_2:def 2 ;
hence H . 1,t = a by A55, A82, FUNCT_4:14; :: thesis:

end;

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