let T be non empty TopSpace; for a, b, c being Point of T
for P1, P2 being Path of a,b
for Q1, Q2 being Path of b,c st a,b are_connected & b,c are_connected & P1,P2 are_homotopic & Q1,Q2 are_homotopic holds
P1 + Q1,P2 + Q2 are_homotopic
let a, b, c be Point of T; for P1, P2 being Path of a,b
for Q1, Q2 being Path of b,c st a,b are_connected & b,c are_connected & P1,P2 are_homotopic & Q1,Q2 are_homotopic holds
P1 + Q1,P2 + Q2 are_homotopic
set BB = [:I[01] ,I[01] :];
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;
let P1, P2 be Path of a,b; for Q1, Q2 being Path of b,c st a,b are_connected & b,c are_connected & P1,P2 are_homotopic & Q1,Q2 are_homotopic holds
P1 + Q1,P2 + Q2 are_homotopic
let Q1, Q2 be Path of b,c; ( a,b are_connected & b,c are_connected & P1,P2 are_homotopic & Q1,Q2 are_homotopic implies P1 + Q1,P2 + Q2 are_homotopic )
assume that
A1:
( a,b are_connected & b,c are_connected )
and
A2:
P1,P2 are_homotopic
and
A3:
Q1,Q2 are_homotopic
; P1 + Q1,P2 + Q2 are_homotopic
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;
A4:
1 is Point of I[01]
by BORSUK_1:86;
A5:
0 is Point of I[01]
by BORSUK_1:86;
then reconsider A01 = [.0 ,1.] as non empty Subset of I[01] by A4, BORSUK_4:49;
A6:
1 / 2 is Point of I[01]
by BORSUK_1:86;
then reconsider B01 = [.0 ,(1 / 2).] as non empty Subset of I[01] by A5, BORSUK_4:49;
reconsider N2 = [:[.(1 / 2),1.],[.0 ,1.]:] as non empty compact Subset of [:I[01] ,I[01] :] by A5, A4, A6, Th13;
reconsider N1 = [:[.0 ,(1 / 2).],[.0 ,1.]:] as non empty compact Subset of [:I[01] ,I[01] :] by A5, A4, A6, Th13;
set T1 = [:I[01] ,I[01] :] | N1;
set T2 = [:I[01] ,I[01] :] | N2;
A01 = [#] I[01]
by BORSUK_1:83;
then A7:
I[01] = I[01] | A01
by TSEP_1:100;
set f1 = [:R1,(id I[01] ):];
set g1 = [:R2,(id I[01] ):];
reconsider f1 = [:R1,(id I[01] ):] as continuous Function of [:(Closed-Interval-TSpace 0 ,(1 / 2)),I[01] :],[:I[01] ,I[01] :] ;
reconsider g1 = [:R2,(id I[01] ):] as continuous Function of [:(Closed-Interval-TSpace (1 / 2),1),I[01] :],[:I[01] ,I[01] :] ;
A8: 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
;
reconsider B02 = [.(1 / 2),1.] as non empty Subset of I[01] by A4, A6, BORSUK_4:49;
consider f being Function of [:I[01] ,I[01] :],T such that
A9:
f is continuous
and
A10:
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 A2, BORSUK_2:def 7;
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 A7, BORSUK_3:26;
then reconsider K1 = f * f1 as continuous Function of ([:I[01] ,I[01] :] | N1),T by A9;
consider g being Function of [:I[01] ,I[01] :],T such that
A11:
g is continuous
and
A12:
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 A3, BORSUK_2:def 7;
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 A7, BORSUK_3:26;
then reconsider K2 = g * g1 as continuous Function of ([:I[01] ,I[01] :] | N2),T by A11;
A13: 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
;
A14:
for p being set st p in ([#] ([:I[01] ,I[01] :] | N1)) /\ ([#] ([:I[01] ,I[01] :] | N2)) holds
K1 . p = K2 . p
proof
A15:
R2 . (1 / 2) = 0
by Th37;
let p be
set ;
( p in ([#] ([:I[01] ,I[01] :] | N1)) /\ ([#] ([:I[01] ,I[01] :] | N2)) implies K1 . p = K2 . p )
A16:
R1 . (1 / 2) = 1
by Th37;
assume
p in ([#] ([:I[01] ,I[01] :] | N1)) /\ ([#] ([:I[01] ,I[01] :] | N2))
;
K1 . p = K2 . p
then
p in [:{(1 / 2)},[.0 ,1.]:]
by Th33;
then consider x,
y being
set such that A17:
x in {(1 / 2)}
and A18:
y in [.0 ,1.]
and A19:
p = [x,y]
by ZFMISC_1:def 2;
A20:
y in the
carrier of
I[01]
by A18, TOPMETR:25, TOPMETR:27;
reconsider y =
y as
Point of
I[01] by A18, TOPMETR:25, TOPMETR:27;
A21:
y in dom (id I[01] )
by A20, FUNCT_2:def 1;
A22:
x = 1
/ 2
by A17, TARSKI:def 1;
then
x in [.(1 / 2),1.]
by XXREAL_1:1;
then A23:
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 A19, A20, ZFMISC_1:106;
then
p in the
carrier of
[:(Closed-Interval-TSpace (1 / 2),1),I[01] :]
by BORSUK_1:def 5;
then A24:
p in dom g1
by FUNCT_2:def 1;
x in [.0 ,(1 / 2).]
by A22, XXREAL_1:1;
then A25:
x in the
carrier of
(Closed-Interval-TSpace 0 ,(1 / 2))
by TOPMETR:25;
then
x in dom R1
by FUNCT_2:def 1;
then A26:
[x,y] in [:(dom R1),(dom (id I[01] )):]
by A21, ZFMISC_1:106;
x in dom R2
by A23, FUNCT_2:def 1;
then A27:
[x,y] in [:(dom R2),(dom (id I[01] )):]
by A21, ZFMISC_1:106;
p in [:the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)),the carrier of I[01] :]
by A19, A20, A25, ZFMISC_1:106;
then
p in the
carrier of
[:(Closed-Interval-TSpace 0 ,(1 / 2)),I[01] :]
by BORSUK_1:def 5;
then
p in dom f1
by FUNCT_2:def 1;
then K1 . p =
f . (f1 . x,y)
by A19, FUNCT_1:23
.=
f . (R1 . x),
((id I[01] ) . y)
by A26, FUNCT_3:86
.=
b
by A10, A22, A16
.=
g . (R2 . x),
((id I[01] ) . y)
by A12, A22, A15
.=
g . (g1 . x,y)
by A27, FUNCT_3:86
.=
K2 . p
by A19, A24, FUNCT_1:23
;
hence
K1 . p = K2 . p
;
verum
end;
([#] ([:I[01] ,I[01] :] | N1)) \/ ([#] ([:I[01] ,I[01] :] | N2)) = [#] [:I[01] ,I[01] :]
by Th32;
then consider h being Function of [:I[01] ,I[01] :],T such that
A28:
h = K1 +* K2
and
A29:
h is continuous
by A14, BORSUK_2:1;
A30: 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
;
A31:
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] ;
( h . s,0 = (P1 + Q1) . s & h . s,1 = (P2 + Q2) . s )
A32:
h . s,1
= (P2 + Q2) . s
proof
per cases
( s < 1 / 2 or s >= 1 / 2 )
;
suppose A33:
s < 1
/ 2
;
h . s,1 = (P2 + Q2) . sthen A34:
2
* s is
Point of
I[01]
by Th6;
A35:
1
in the
carrier of
I[01]
by BORSUK_1:86;
then A36:
1
in dom (id I[01] )
by FUNCT_2:def 1;
A37:
s >= 0
by BORSUK_1:86;
then A38:
R1 . s =
(((1 - 0 ) / ((1 / 2) - 0 )) * (s - 0 )) + 0
by A33, Th39
.=
2
* s
;
s in [.0 ,(1 / 2).]
by A33, A37, XXREAL_1:1;
then A39:
s in the
carrier of
(Closed-Interval-TSpace 0 ,(1 / 2))
by TOPMETR:25;
then A40:
[s,1] in dom f1
by A30, A35, ZFMISC_1:106;
s in dom R1
by A39, FUNCT_2:def 1;
then A41:
[s,1] in [:(dom R1),(dom (id I[01] )):]
by A36, ZFMISC_1:106;
not
s in [.(1 / 2),1.]
by A33, XXREAL_1:1;
then
not
s in the
carrier of
(Closed-Interval-TSpace (1 / 2),1)
by TOPMETR:25;
then
not
[s,1] in dom K2
by A13, ZFMISC_1:106;
then h . s,1 =
K1 . s,1
by A28, FUNCT_4:12
.=
f . (f1 . s,1)
by A40, FUNCT_1:23
.=
f . (R1 . s),
((id I[01] ) . 1)
by A41, FUNCT_3:86
.=
f . (2 * s),1
by A4, A38, FUNCT_1:35
.=
P2 . (2 * s)
by A10, A34
;
hence
h . s,1
= (P2 + Q2) . s
by A1, A33, BORSUK_2:def 5;
verum end; suppose A42:
s >= 1
/ 2
;
h . s,1 = (P2 + Q2) . sA43:
s <= 1
by BORSUK_1:86;
then A44:
R2 . s =
(((1 - 0 ) / (1 - (1 / 2))) * (s - (1 / 2))) + 0
by A42, Th39
.=
(2 * s) - 1
;
A45:
(2 * s) - 1 is
Point of
I[01]
by A42, Th7;
A46:
1
in the
carrier of
I[01]
by BORSUK_1:86;
then A47:
1
in dom (id I[01] )
by FUNCT_2:def 1;
s in [.(1 / 2),1.]
by A42, A43, XXREAL_1:1;
then A48:
s in the
carrier of
(Closed-Interval-TSpace (1 / 2),1)
by TOPMETR:25;
then A49:
[s,1] in dom g1
by A8, A46, ZFMISC_1:106;
s in dom R2
by A48, FUNCT_2:def 1;
then A50:
[s,1] in [:(dom R2),(dom (id I[01] )):]
by A47, ZFMISC_1:106;
[s,1] in dom K2
by A13, A48, A46, ZFMISC_1:106;
then h . s,1 =
K2 . s,1
by A28, FUNCT_4:14
.=
g . (g1 . s,1)
by A49, FUNCT_1:23
.=
g . (R2 . s),
((id I[01] ) . 1)
by A50, FUNCT_3:86
.=
g . ((2 * s) - 1),1
by A4, A44, FUNCT_1:35
.=
Q2 . ((2 * s) - 1)
by A12, A45
;
hence
h . s,1
= (P2 + Q2) . s
by A1, A42, BORSUK_2:def 5;
verum end;
end;
h . s,
0 = (P1 + Q1) . s
proof
per cases
( s < 1 / 2 or s >= 1 / 2 )
;
suppose A51:
s < 1
/ 2
;
h . s,0 = (P1 + Q1) . sthen A52:
2
* s is
Point of
I[01]
by Th6;
A53:
0 in the
carrier of
I[01]
by BORSUK_1:86;
then A54:
0 in dom (id I[01] )
by FUNCT_2:def 1;
A55:
s >= 0
by BORSUK_1:86;
then A56:
R1 . s =
(((1 - 0 ) / ((1 / 2) - 0 )) * (s - 0 )) + 0
by A51, Th39
.=
2
* s
;
s in [.0 ,(1 / 2).]
by A51, A55, XXREAL_1:1;
then A57:
s in the
carrier of
(Closed-Interval-TSpace 0 ,(1 / 2))
by TOPMETR:25;
then A58:
[s,0 ] in dom f1
by A30, A53, ZFMISC_1:106;
s in dom R1
by A57, FUNCT_2:def 1;
then A59:
[s,0 ] in [:(dom R1),(dom (id I[01] )):]
by A54, ZFMISC_1:106;
not
s in [.(1 / 2),1.]
by A51, XXREAL_1:1;
then
not
s in the
carrier of
(Closed-Interval-TSpace (1 / 2),1)
by TOPMETR:25;
then
not
[s,0 ] in dom K2
by A13, ZFMISC_1:106;
then h . s,
0 =
K1 . s,
0
by A28, FUNCT_4:12
.=
f . (f1 . s,0 )
by A58, FUNCT_1:23
.=
f . (R1 . s),
((id I[01] ) . 0 )
by A59, FUNCT_3:86
.=
f . (2 * s),
0
by A5, A56, FUNCT_1:35
.=
P1 . (2 * s)
by A10, A52
;
hence
h . s,
0 = (P1 + Q1) . s
by A1, A51, BORSUK_2:def 5;
verum end; suppose A60:
s >= 1
/ 2
;
h . s,0 = (P1 + Q1) . sA61:
s <= 1
by BORSUK_1:86;
then A62:
R2 . s =
(((1 - 0 ) / (1 - (1 / 2))) * (s - (1 / 2))) + 0
by A60, Th39
.=
(2 * s) - 1
;
A63:
(2 * s) - 1 is
Point of
I[01]
by A60, Th7;
A64:
0 in the
carrier of
I[01]
by BORSUK_1:86;
then A65:
0 in dom (id I[01] )
by FUNCT_2:def 1;
s in [.(1 / 2),1.]
by A60, A61, XXREAL_1:1;
then A66:
s in the
carrier of
(Closed-Interval-TSpace (1 / 2),1)
by TOPMETR:25;
then A67:
[s,0 ] in dom g1
by A8, A64, ZFMISC_1:106;
s in dom R2
by A66, FUNCT_2:def 1;
then A68:
[s,0 ] in [:(dom R2),(dom (id I[01] )):]
by A65, ZFMISC_1:106;
[s,0 ] in dom K2
by A13, A66, A64, ZFMISC_1:106;
then h . s,
0 =
K2 . s,
0
by A28, FUNCT_4:14
.=
g . (g1 . s,0 )
by A67, FUNCT_1:23
.=
g . (R2 . s),
((id I[01] ) . 0 )
by A68, FUNCT_3:86
.=
g . ((2 * s) - 1),
0
by A5, A62, FUNCT_1:35
.=
Q1 . ((2 * s) - 1)
by A12, A63
;
hence
h . s,
0 = (P1 + Q1) . s
by A1, A60, BORSUK_2:def 5;
verum end;
end;
hence
(
h . s,
0 = (P1 + Q1) . s &
h . s,1
= (P2 + Q2) . s )
by A32;
verum
end;
take
h
; BORSUK_2:def 7 ( h is continuous & ( for b1 being Element of the carrier of I[01] holds
( h . b1,0 = (P1 + Q1) . b1 & h . b1,1 = (P2 + Q2) . b1 & h . 0 ,b1 = a & h . 1,b1 = c ) ) )
for t being Point of I[01] holds
( h . 0 ,t = a & h . 1,t = c )
proof
let t be
Point of
I[01] ;
( h . 0 ,t = a & h . 1,t = c )
A69:
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
;
t in the
carrier of
I[01]
;
then A70:
t in dom (id I[01] )
by FUNCT_2:def 1;
0 in [.0 ,(1 / 2).]
by XXREAL_1:1;
then A71:
0 in the
carrier of
(Closed-Interval-TSpace 0 ,(1 / 2))
by TOPMETR:25;
then A72:
[0 ,t] in dom f1
by A30, ZFMISC_1:106;
0 in dom R1
by A71, FUNCT_2:def 1;
then A73:
[0 ,t] in [:(dom R1),(dom (id I[01] )):]
by A70, ZFMISC_1:106;
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
not
[0 ,t] in dom K2
by A69, ZFMISC_1:106;
hence h . 0 ,
t =
K1 . 0 ,
t
by A28, FUNCT_4:12
.=
f . (f1 . 0 ,t)
by A72, FUNCT_1:23
.=
f . (R1 . 0 ),
((id I[01] ) . t)
by A73, FUNCT_3:86
.=
f . (R1 . 0 ),
t
by FUNCT_1:35
.=
f . 0 ,
t
by Th37
.=
a
by A10
;
h . 1,t = c
t in the
carrier of
I[01]
;
then A74:
t in dom (id I[01] )
by FUNCT_2:def 1;
1
in [.(1 / 2),1.]
by XXREAL_1:1;
then A75:
1
in the
carrier of
(Closed-Interval-TSpace (1 / 2),1)
by TOPMETR:25;
then
1
in dom R2
by FUNCT_2:def 1;
then A76:
[1,t] in [:(dom R2),(dom (id I[01] )):]
by A74, 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 A77:
[1,t] in dom g1
by A8, ZFMISC_1:106;
[1,t] in dom K2
by A69, A75, ZFMISC_1:106;
then h . 1,
t =
K2 . 1,
t
by A28, FUNCT_4:14
.=
g . (g1 . 1,t)
by A77, FUNCT_1:23
.=
g . (R2 . 1),
((id I[01] ) . t)
by A76, FUNCT_3:86
.=
g . (R2 . 1),
t
by FUNCT_1:35
.=
g . 1,
t
by Th37
.=
c
by A12
;
hence
h . 1,
t = c
;
verum
end;
hence
( h is continuous & ( for b1 being Element of the carrier of I[01] holds
( h . b1,0 = (P1 + Q1) . b1 & h . b1,1 = (P2 + Q2) . b1 & h . 0 ,b1 = a & h . 1,b1 = c ) ) )
by A29, A31; verum