let T be non empty TopSpace; :: thesis:
let a, b, c be Point of T; :: thesis:
let P1, P2 be Path of a,b; :: thesis:
let Q1, Q2 be Path of b,c; :: thesis:
assume that
A1: a,b are_connected and
A2: b,c are_connected and
A3: P1,P2 are_homotopic and
A4: Q1,Q2 are_homotopic ; :: thesis:
consider f being Function of [:I[01] ,I[01] :],T such that
A5: ( f is continuous & ( for s being Point of I[01] holds
( f . s,0 = P1 . s & f . s,1 = P2 . s & ( for t being Point of I[01] holds
( f . 0 ,t = a & f . 1,t = b ) ) ) ) ) by A3, BORSUK_2:def 7;
consider g being Function of [:I[01] ,I[01] :],T such that
A6: ( g is continuous & ( for s being Point of I[01] holds
( g . s,0 = Q1 . s & g . s,1 = Q2 . s & ( for t being Point of I[01] holds
( g . 0 ,t = b & g . 1,t = c ) ) ) ) ) by A4, BORSUK_2:def 7;
reconsider R1 = L[01] 0 ,(1 / 2),0 ,1 as continuous Function of (Closed-Interval-TSpace 0 ,(1 / 2)),I[01] by Th38, TOPMETR:27;
reconsider R2 = L[01] (1 / 2),1,0 ,1 as continuous Function of (Closed-Interval-TSpace (1 / 2),1),I[01] by Th38, TOPMETR:27;
set f1 = [:R1,(id I[01] ):];
set g1 = [:R2,(id I[01] ):];
set BB = [:I[01] ,I[01] :];
A7: ( 0 is Point of I[01] & 1 is Point of I[01] & 1 / 2 is Point of I[01] ) by BORSUK_1:86;
then reconsider N1 = [:[.0 ,(1 / 2).],[.0 ,1.]:] as non empty compact Subset of [:I[01] ,I[01] :] by Th13;
reconsider N2 = [:[.(1 / 2),1.],[.0 ,1.]:] as non empty compact Subset of [:I[01] ,I[01] :] by A7, Th13;
set T1 = [:I[01] ,I[01] :] | N1;
set T2 = [:I[01] ,I[01] :] | N2;
reconsider f1 = [:R1,(id I[01] ):] as continuous Function of [:(Closed-Interval-TSpace 0 ,(1 / 2)),I[01] :],[:I[01] ,I[01] :] by BORSUK_2:12;
reconsider A01 = [.0 ,1.] as non empty Subset of I[01] by A7, BORSUK_4:49;
reconsider B01 = [.0 ,(1 / 2).] as non empty Subset of I[01] by A7, BORSUK_4:49;
reconsider B02 = [.(1 / 2),1.] as non empty Subset of I[01] by A7, BORSUK_4:49;
A01 = [#] I[01] by BORSUK_1:83;
then A8: I[01] = I[01] | A01 by TSEP_1:100;
Closed-Interval-TSpace 0 ,(1 / 2) = I[01] | B01 by TOPMETR:31;
then [:I[01] ,I[01] :] | N1 = [:(Closed-Interval-TSpace 0 ,(1 / 2)),I[01] :] by A8, BORSUK_3:26;
then reconsider K1 = f * f1 as continuous Function of ([:I[01] ,I[01] :] | N1),T by A5;
reconsider g1 = [:R2,(id I[01] ):] as continuous Function of [:(Closed-Interval-TSpace (1 / 2),1),I[01] :],[:I[01] ,I[01] :] by BORSUK_2:12;
Closed-Interval-TSpace (1 / 2),1 = I[01] | B02 by TOPMETR:31;
then [:I[01] ,I[01] :] | N2 = [:(Closed-Interval-TSpace (1 / 2),1),I[01] :] by A8, BORSUK_3:26;
then reconsider K2 = g * g1 as continuous Function of ([:I[01] ,I[01] :] | N2),T by A6;
A9: ([#] ([:I[01] ,I[01] :] | N1)) \/ ([#] ([:I[01] ,I[01] :] | N2)) = [#] [:I[01] ,I[01] :] by Th32;
A10: dom K2 = the carrier of [:(Closed-Interval-TSpace (1 / 2),1),I[01] :] by FUNCT_2:def 1
.= [:the carrier of (Closed-Interval-TSpace (1 / 2),1),the carrier of I[01] :] by BORSUK_1:def 5 ;
A11: dom f1 = the carrier of [:(Closed-Interval-TSpace 0 ,(1 / 2)),I[01] :] by FUNCT_2:def 1
.= [:the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)),the carrier of I[01] :] by BORSUK_1:def 5 ;
A12: dom g1 = the carrier of [:(Closed-Interval-TSpace (1 / 2),1),I[01] :] by FUNCT_2:def 1
.= [:the carrier of (Closed-Interval-TSpace (1 / 2),1),the carrier of I[01] :] by BORSUK_1:def 5 ;
for p being set st p in ([#] ([:I[01] ,I[01] :] | N1)) /\ ([#] ([:I[01] ,I[01] :] | N2)) holds
K1 . p = K2 . p

proof

let p be set ; :: thesis:
assume p in ([#] ([:I[01] ,I[01] :] | N1)) /\ ([#] ([:I[01] ,I[01] :] | N2)) ; :: thesis:
then p in [:{(1 / 2)},[.0 ,1.]:] by Th33;
then consider x, y being set such that
A13: ( x in {(1 / 2)} & y in [.0 ,1.] & p = [x,y] ) by ZFMISC_1:def 2;
A14: y in the carrier of I[01] by A13, TOPMETR:25, TOPMETR:27;
reconsider y = y as Point of I[01] by A13, TOPMETR:25, TOPMETR:27;
A15: x = 1 / 2 by A13, TARSKI:def 1;
then x in [.0 ,(1 / 2).] by XXREAL_1:1;
then A16: x in the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) by TOPMETR:25;
then p in [:the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)),the carrier of I[01] :] by A13, A14, ZFMISC_1:106;
then p in the carrier of [:(Closed-Interval-TSpace 0 ,(1 / 2)),I[01] :] by BORSUK_1:def 5;
then A17: p in dom f1 by FUNCT_2:def 1;
x in [.(1 / 2),1.] by A15, XXREAL_1:1;
then A18: x in the carrier of (Closed-Interval-TSpace (1 / 2),1) by TOPMETR:25;
then p in [:the carrier of (Closed-Interval-TSpace (1 / 2),1),the carrier of I[01] :] by A13, A14, ZFMISC_1:106;
then p in the carrier of [:(Closed-Interval-TSpace (1 / 2),1),I[01] :] by BORSUK_1:def 5;
then A19: p in dom g1 by FUNCT_2:def 1;
A20: x in dom R1 by A16, FUNCT_2:def 1;
A21: y in dom (id I[01] ) by A14, FUNCT_2:def 1;
then A22: [x,y] in [:(dom R1),(dom (id I[01] )):] by A20, ZFMISC_1:106;
x in dom R2 by A18, FUNCT_2:def 1;
then A23: [x,y] in [:(dom R2),(dom (id I[01] )):] by A21, ZFMISC_1:106;
A24: R1 . (1 / 2) = 1 by Th37;
A25: R2 . (1 / 2) = 0 by Th37;
K1 . p = f . (f1 . x,y) by A13, A17, FUNCT_1:23
.= f . (R1 . x),((id I[01] ) . y) by A22, FUNCT_3:86
.= b by A5, A15, A24
.= g . (R2 . x),((id I[01] ) . y) by A6, A15, A25
.= g . (g1 . x,y) by A23, FUNCT_3:86
.= K2 . p by A13, A19, FUNCT_1:23 ;
hence K1 . p = K2 . p ; :: thesis:

end;

then consider h being Function of [:I[01] ,I[01] :],T such that
A26: ( h = K1 +* K2 & h is continuous ) by A9, BORSUK_2:1;
take h ; :: according to BORSUK_2:def 7 :: thesis:
A27: for s being Point of I[01] holds
( h . s,0 = (P1 + Q1) . s & h . s,1 = (P2 + Q2) . s )

proof

let s be Point of I[01] ; :: thesis:
A28: h . s,0 = (P1 + Q1) . s

proof

per cases ;

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

A30: s >= 0 by BORSUK_1:86;
not s in [.(1 / 2),1.] by A29, XXREAL_1:1;
then not s in the carrier of (Closed-Interval-TSpace (1 / 2),1) by TOPMETR:25;
then A31: not [s,0 ] in dom K2 by A10, ZFMISC_1:106;
s in [.0 ,(1 / 2).] by A29, A30, XXREAL_1:1;
then A32: ( s in the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) & 0 in the carrier of I[01] ) by BORSUK_1:86, TOPMETR:25;
then A33: [s,0 ] in dom f1 by A11, ZFMISC_1:106;
A34: s in dom R1 by A32, FUNCT_2:def 1;
0 in dom (id I[01] ) by A32, FUNCT_2:def 1;
then A35: [s,0 ] in [:(dom R1),(dom (id I[01] )):] by A34, ZFMISC_1:106;
A36: R1 . s = (((1 - 0 ) / ((1 / 2) - 0 )) * (s - 0 )) + 0 by A29, A30, Th39
.= 2 * s ;
A37: 2 * s is Point of I[01] by A29, Th6;
h . s,0 = K1 . s,0 by A26, A31, FUNCT_4:12
.= f . (f1 . s,0 ) by A33, FUNCT_1:23
.= f . (R1 . s),((id I[01] ) . 0 ) by A35, FUNCT_3:86
.= f . (2 * s),0 by A7, A36, TMAP_1:91
.= P1 . (2 * s) by A5, A37 ;
hence h . s,0 = (P1 + Q1) . s by A1, A2, A29, BORSUK_2:def 5; :: thesis:

end;

suppose A38: s >= 1 / 2 ; :: thesis:

A39: s <= 1 by BORSUK_1:86;
then s in [.(1 / 2),1.] by A38, XXREAL_1:1;
then A40: ( s in the carrier of (Closed-Interval-TSpace (1 / 2),1) & 0 in the carrier of I[01] ) by BORSUK_1:86, TOPMETR:25;
then A41: [s,0 ] in dom K2 by A10, ZFMISC_1:106;
A42: [s,0 ] in dom g1 by A12, A40, ZFMISC_1:106;
A43: s in dom R2 by A40, FUNCT_2:def 1;
0 in dom (id I[01] ) by A40, FUNCT_2:def 1;
then A44: [s,0 ] in [:(dom R2),(dom (id I[01] )):] by A43, ZFMISC_1:106;
A45: R2 . s = (((1 - 0 ) / (1 - (1 / 2))) * (s - (1 / 2))) + 0 by A38, A39, Th39
.= (2 * s) - 1 ;
A46: (2 * s) - 1 is Point of I[01] by A38, Th7;
h . s,0 = K2 . s,0 by A26, A41, FUNCT_4:14
.= g . (g1 . s,0 ) by A42, FUNCT_1:23
.= g . (R2 . s),((id I[01] ) . 0 ) by A44, FUNCT_3:86
.= g . ((2 * s) - 1),0 by A7, A45, TMAP_1:91
.= Q1 . ((2 * s) - 1) by A6, A46 ;
hence h . s,0 = (P1 + Q1) . s by A1, A2, A38, BORSUK_2:def 5; :: thesis:

end;

h . s,1 = (P2 + Q2) . s

proof

per cases ;

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

A48: s >= 0 by BORSUK_1:86;
not s in [.(1 / 2),1.] by A47, XXREAL_1:1;
then not s in the carrier of (Closed-Interval-TSpace (1 / 2),1) by TOPMETR:25;
then A49: not [s,1] in dom K2 by A10, ZFMISC_1:106;
s in [.0 ,(1 / 2).] by A47, A48, XXREAL_1:1;
then A50: ( s in the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) & 1 in the carrier of I[01] ) by BORSUK_1:86, TOPMETR:25;
then A51: [s,1] in dom f1 by A11, ZFMISC_1:106;
A52: s in dom R1 by A50, FUNCT_2:def 1;
1 in dom (id I[01] ) by A50, FUNCT_2:def 1;
then A53: [s,1] in [:(dom R1),(dom (id I[01] )):] by A52, ZFMISC_1:106;
A54: R1 . s = (((1 - 0 ) / ((1 / 2) - 0 )) * (s - 0 )) + 0 by A47, A48, Th39
.= 2 * s ;
A55: 2 * s is Point of I[01] by A47, Th6;
h . s,1 = K1 . s,1 by A26, A49, FUNCT_4:12
.= f . (f1 . s,1) by A51, FUNCT_1:23
.= f . (R1 . s),((id I[01] ) . 1) by A53, FUNCT_3:86
.= f . (2 * s),1 by A7, A54, TMAP_1:91
.= P2 . (2 * s) by A5, A55 ;
hence h . s,1 = (P2 + Q2) . s by A1, A2, A47, BORSUK_2:def 5; :: thesis:

end;

suppose A56: s >= 1 / 2 ; :: thesis:

A57: s <= 1 by BORSUK_1:86;
then s in [.(1 / 2),1.] by A56, XXREAL_1:1;
then A58: ( s in the carrier of (Closed-Interval-TSpace (1 / 2),1) & 1 in the carrier of I[01] ) by BORSUK_1:86, TOPMETR:25;
then A59: [s,1] in dom K2 by A10, ZFMISC_1:106;
A60: [s,1] in dom g1 by A12, A58, ZFMISC_1:106;
A61: s in dom R2 by A58, FUNCT_2:def 1;
1 in dom (id I[01] ) by A58, FUNCT_2:def 1;
then A62: [s,1] in [:(dom R2),(dom (id I[01] )):] by A61, ZFMISC_1:106;
A63: R2 . s = (((1 - 0 ) / (1 - (1 / 2))) * (s - (1 / 2))) + 0 by A56, A57, Th39
.= (2 * s) - 1 ;
A64: (2 * s) - 1 is Point of I[01] by A56, Th7;
h . s,1 = K2 . s,1 by A26, A59, FUNCT_4:14
.= g . (g1 . s,1) by A60, FUNCT_1:23
.= g . (R2 . s),((id I[01] ) . 1) by A62, FUNCT_3:86
.= g . ((2 * s) - 1),1 by A7, A63, TMAP_1:91
.= Q2 . ((2 * s) - 1) by A6, A64 ;
hence h . s,1 = (P2 + Q2) . s by A1, A2, A56, BORSUK_2:def 5; :: thesis:

end;

hence ( h . s,0 = (P1 + Q1) . s & h . s,1 = (P2 + Q2) . s ) by A28; :: thesis:

end;

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

proof

let t be Point of I[01] ; :: thesis:
A65: dom K2 = the carrier of [:(Closed-Interval-TSpace (1 / 2),1),I[01] :] by FUNCT_2:def 1
.= [:the carrier of (Closed-Interval-TSpace (1 / 2),1),the carrier of I[01] :] by BORSUK_1:def 5 ;
not 0 in [.(1 / 2),1.] by XXREAL_1:1;
then not 0 in the carrier of (Closed-Interval-TSpace (1 / 2),1) by TOPMETR:25;
then A66: not [0 ,t] in dom K2 by A65, ZFMISC_1:106;
1 in [.(1 / 2),1.] by XXREAL_1:1;
then A67: 1 in the carrier of (Closed-Interval-TSpace (1 / 2),1) by TOPMETR:25;
then A68: [1,t] in dom K2 by A65, ZFMISC_1:106;
0 in [.0 ,(1 / 2).] by XXREAL_1:1;
then A69: 0 in the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) by TOPMETR:25;
then A70: 0 in dom R1 by FUNCT_2:def 1;
A71: t in the carrier of I[01] ;
A72: [0 ,t] in dom f1 by A11, A69, ZFMISC_1:106;
1 in [.(1 / 2),1.] by XXREAL_1:1;
then 1 in the carrier of (Closed-Interval-TSpace (1 / 2),1) by TOPMETR:25;
then A73: [1,t] in dom g1 by A12, ZFMISC_1:106;
t in dom (id I[01] ) by A71, FUNCT_2:def 1;
then A74: [0 ,t] in [:(dom R1),(dom (id I[01] )):] by A70, ZFMISC_1:106;
A75: 1 in dom R2 by A67, FUNCT_2:def 1;
t in the carrier of I[01] ;
then t in dom (id I[01] ) by FUNCT_2:def 1;
then A76: [1,t] in [:(dom R2),(dom (id I[01] )):] by A75, ZFMISC_1:106;
thus h . 0 ,t = K1 . 0 ,t by A26, A66, FUNCT_4:12
.= f . (f1 . 0 ,t) by A72, FUNCT_1:23
.= f . (R1 . 0 ),((id I[01] ) . t) by A74, FUNCT_3:86
.= f . (R1 . 0 ),t by TMAP_1:91
.= f . 0 ,t by Th37
.= a by A5 ; :: thesis:
h . 1,t = K2 . 1,t by A26, A68, FUNCT_4:14
.= g . (g1 . 1,t) by A73, FUNCT_1:23
.= g . (R2 . 1),((id I[01] ) . t) by A76, FUNCT_3:86
.= g . (R2 . 1),t by TMAP_1:91
.= g . 1,t by Th37
.= c by A6 ;
hence h . 1,t = c ; :: thesis:

end;

hence ( h is continuous & ( for b₁ being Element of the carrier of I[01] holds
( h . b₁,0 = (P1 + Q1) . b₁ & h . b₁,1 = (P2 + Q2) . b₁ & h . 0 ,b₁ = a & h . 1,b₁ = c ) ) ) by A26, A27; :: thesis: