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 Th34, TOPMETR:20;
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 Th34, TOPMETR:20;
A4:
1 is Point of I[01]
by BORSUK_1:43;
A5:
0 is Point of I[01]
by BORSUK_1:43;
then reconsider A01 = [.0,1.] as non empty Subset of I[01] by A4, BORSUK_4:24;
A6:
1 / 2 is Point of I[01]
by BORSUK_1:43;
then reconsider B01 = [.0,(1 / 2).] as non empty Subset of I[01] by A5, BORSUK_4:24;
reconsider N2 = [:[.(1 / 2),1.],[.0,1.]:] as non empty compact Subset of [:I[01],I[01]:] by A5, A4, A6, Th9;
reconsider N1 = [:[.0,(1 / 2).],[.0,1.]:] as non empty compact Subset of [:I[01],I[01]:] by A5, A4, A6, Th9;
set T1 = [:I[01],I[01]:] | N1;
set T2 = [:I[01],I[01]:] | N2;
A01 = [#] I[01]
by BORSUK_1:40;
then A7:
I[01] = I[01] | A01
by TSEP_1:93;
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 2
;
reconsider B02 = [.(1 / 2),1.] as non empty Subset of I[01] by A4, A6, BORSUK_4:24;
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;
Closed-Interval-TSpace (0,(1 / 2)) = I[01] | B01
by TOPMETR:24;
then
[:I[01],I[01]:] | N1 = [:(Closed-Interval-TSpace (0,(1 / 2))),I[01]:]
by A7, BORSUK_3:22;
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;
Closed-Interval-TSpace ((1 / 2),1) = I[01] | B02
by TOPMETR:24;
then
[:I[01],I[01]:] | N2 = [:(Closed-Interval-TSpace ((1 / 2),1)),I[01]:]
by A7, BORSUK_3:22;
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 2
;
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 Th33;
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 Th33;
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 Th29;
then consider x,
y being
object 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:18, TOPMETR:20;
reconsider y =
y as
Point of
I[01] by A18, TOPMETR:18, TOPMETR:20;
A21:
x = 1
/ 2
by A17, TARSKI:def 1;
then
x in [.(1 / 2),1.]
by XXREAL_1:1;
then A22:
x in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then
p in [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of I[01]:]
by A19, A20, ZFMISC_1:87;
then
p in the
carrier of
[:(Closed-Interval-TSpace ((1 / 2),1)),I[01]:]
by BORSUK_1:def 2;
then A23:
p in dom g1
by FUNCT_2:def 1;
x in [.0,(1 / 2).]
by A21, XXREAL_1:1;
then A24:
x in the
carrier of
(Closed-Interval-TSpace (0,(1 / 2)))
by TOPMETR:18;
then
x in dom R1
by FUNCT_2:def 1;
then A25:
[x,y] in [:(dom R1),(dom (id I[01])):]
by ZFMISC_1:87;
x in dom R2
by A22, FUNCT_2:def 1;
then A26:
[x,y] in [:(dom R2),(dom (id I[01])):]
by ZFMISC_1:87;
p in [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of I[01]:]
by A19, A20, A24, ZFMISC_1:87;
then
p in the
carrier of
[:(Closed-Interval-TSpace (0,(1 / 2))),I[01]:]
by BORSUK_1:def 2;
then
p in dom f1
by FUNCT_2:def 1;
then K1 . p =
f . (f1 . (x,y))
by A19, FUNCT_1:13
.=
f . (
(R1 . x),
((id I[01]) . y))
by A25, FUNCT_3:65
.=
b
by A10, A21, A16
.=
g . (
(R2 . x),
((id I[01]) . y))
by A12, A21, A15
.=
g . (g1 . (x,y))
by A26, FUNCT_3:65
.=
K2 . p
by A19, A23, FUNCT_1:13
;
hence
K1 . p = K2 . p
;
verum
end;
([#] ([:I[01],I[01]:] | N1)) \/ ([#] ([:I[01],I[01]:] | N2)) = [#] [:I[01],I[01]:]
by Th28;
then consider h being Function of [:I[01],I[01]:],T such that
A27:
h = K1 +* K2
and
A28:
h is continuous
by A14, BORSUK_2:1;
A29: 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 2
;
A30:
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 )
A31:
h . (
s,1)
= (P2 + Q2) . s
proof
per cases
( s < 1 / 2 or s >= 1 / 2 )
;
suppose A32:
s < 1
/ 2
;
h . (s,1) = (P2 + Q2) . sthen A33:
2
* s is
Point of
I[01]
by Th3;
A34:
1
in the
carrier of
I[01]
by BORSUK_1:43;
then A35:
1
in dom (id I[01])
;
A36:
s >= 0
by BORSUK_1:43;
then A37:
R1 . s =
(((1 - 0) / ((1 / 2) - 0)) * (s - 0)) + 0
by A32, Th35
.=
2
* s
;
s in [.0,(1 / 2).]
by A32, A36, XXREAL_1:1;
then A38:
s in the
carrier of
(Closed-Interval-TSpace (0,(1 / 2)))
by TOPMETR:18;
then A39:
[s,1] in dom f1
by A29, A34, ZFMISC_1:87;
s in dom R1
by A38, FUNCT_2:def 1;
then A40:
[s,1] in [:(dom R1),(dom (id I[01])):]
by A35, ZFMISC_1:87;
not
s in [.(1 / 2),1.]
by A32, XXREAL_1:1;
then
not
s in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then
not
[s,1] in dom K2
by A13, ZFMISC_1:87;
then h . (
s,1) =
K1 . (
s,1)
by A27, FUNCT_4:11
.=
f . (f1 . (s,1))
by A39, FUNCT_1:13
.=
f . (
(R1 . s),
((id I[01]) . 1))
by A40, FUNCT_3:65
.=
f . (
(2 * s),1)
by A4, A37, FUNCT_1:18
.=
P2 . (2 * s)
by A10, A33
;
hence
h . (
s,1)
= (P2 + Q2) . s
by A1, A32, BORSUK_2:def 5;
verum end; suppose A41:
s >= 1
/ 2
;
h . (s,1) = (P2 + Q2) . sA42:
s <= 1
by BORSUK_1:43;
then A43:
R2 . s =
(((1 - 0) / (1 - (1 / 2))) * (s - (1 / 2))) + 0
by A41, Th35
.=
(2 * s) - 1
;
A44:
(2 * s) - 1 is
Point of
I[01]
by A41, Th4;
A45:
1
in the
carrier of
I[01]
by BORSUK_1:43;
then A46:
1
in dom (id I[01])
;
s in [.(1 / 2),1.]
by A41, A42, XXREAL_1:1;
then A47:
s in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then A48:
[s,1] in dom g1
by A8, A45, ZFMISC_1:87;
s in dom R2
by A47, FUNCT_2:def 1;
then A49:
[s,1] in [:(dom R2),(dom (id I[01])):]
by A46, ZFMISC_1:87;
[s,1] in dom K2
by A13, A47, A45, ZFMISC_1:87;
then h . (
s,1) =
K2 . (
s,1)
by A27, FUNCT_4:13
.=
g . (g1 . (s,1))
by A48, FUNCT_1:13
.=
g . (
(R2 . s),
((id I[01]) . 1))
by A49, FUNCT_3:65
.=
g . (
((2 * s) - 1),1)
by A4, A43, FUNCT_1:18
.=
Q2 . ((2 * s) - 1)
by A12, A44
;
hence
h . (
s,1)
= (P2 + Q2) . s
by A1, A41, BORSUK_2:def 5;
verum end;
end;
h . (
s,
0)
= (P1 + Q1) . s
proof
per cases
( s < 1 / 2 or s >= 1 / 2 )
;
suppose A50:
s < 1
/ 2
;
h . (s,0) = (P1 + Q1) . sthen A51:
2
* s is
Point of
I[01]
by Th3;
A52:
0 in the
carrier of
I[01]
by BORSUK_1:43;
then A53:
0 in dom (id I[01])
;
A54:
s >= 0
by BORSUK_1:43;
then A55:
R1 . s =
(((1 - 0) / ((1 / 2) - 0)) * (s - 0)) + 0
by A50, Th35
.=
2
* s
;
s in [.0,(1 / 2).]
by A50, A54, XXREAL_1:1;
then A56:
s in the
carrier of
(Closed-Interval-TSpace (0,(1 / 2)))
by TOPMETR:18;
then A57:
[s,0] in dom f1
by A29, A52, ZFMISC_1:87;
s in dom R1
by A56, FUNCT_2:def 1;
then A58:
[s,0] in [:(dom R1),(dom (id I[01])):]
by A53, ZFMISC_1:87;
not
s in [.(1 / 2),1.]
by A50, XXREAL_1:1;
then
not
s in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then
not
[s,0] in dom K2
by A13, ZFMISC_1:87;
then h . (
s,
0) =
K1 . (
s,
0)
by A27, FUNCT_4:11
.=
f . (f1 . (s,0))
by A57, FUNCT_1:13
.=
f . (
(R1 . s),
((id I[01]) . 0))
by A58, FUNCT_3:65
.=
f . (
(2 * s),
0)
by A5, A55, FUNCT_1:18
.=
P1 . (2 * s)
by A10, A51
;
hence
h . (
s,
0)
= (P1 + Q1) . s
by A1, A50, BORSUK_2:def 5;
verum end; suppose A59:
s >= 1
/ 2
;
h . (s,0) = (P1 + Q1) . sA60:
s <= 1
by BORSUK_1:43;
then A61:
R2 . s =
(((1 - 0) / (1 - (1 / 2))) * (s - (1 / 2))) + 0
by A59, Th35
.=
(2 * s) - 1
;
A62:
(2 * s) - 1 is
Point of
I[01]
by A59, Th4;
A63:
0 in the
carrier of
I[01]
by BORSUK_1:43;
then A64:
0 in dom (id I[01])
;
s in [.(1 / 2),1.]
by A59, A60, XXREAL_1:1;
then A65:
s in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then A66:
[s,0] in dom g1
by A8, A63, ZFMISC_1:87;
s in dom R2
by A65, FUNCT_2:def 1;
then A67:
[s,0] in [:(dom R2),(dom (id I[01])):]
by A64, ZFMISC_1:87;
[s,0] in dom K2
by A13, A65, A63, ZFMISC_1:87;
then h . (
s,
0) =
K2 . (
s,
0)
by A27, FUNCT_4:13
.=
g . (g1 . (s,0))
by A66, FUNCT_1:13
.=
g . (
(R2 . s),
((id I[01]) . 0))
by A67, FUNCT_3:65
.=
g . (
((2 * s) - 1),
0)
by A5, A61, FUNCT_1:18
.=
Q1 . ((2 * s) - 1)
by A12, A62
;
hence
h . (
s,
0)
= (P1 + Q1) . s
by A1, A59, BORSUK_2:def 5;
verum end;
end;
hence
(
h . (
s,
0)
= (P1 + Q1) . s &
h . (
s,1)
= (P2 + Q2) . s )
by A31;
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 )
A68:
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 2
;
0 in [.0,(1 / 2).]
by XXREAL_1:1;
then A69:
0 in the
carrier of
(Closed-Interval-TSpace (0,(1 / 2)))
by TOPMETR:18;
then A70:
[0,t] in dom f1
by A29, ZFMISC_1:87;
0 in dom R1
by A69, FUNCT_2:def 1;
then A71:
[0,t] in [:(dom R1),(dom (id I[01])):]
by ZFMISC_1:87;
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:18;
then
not
[0,t] in dom K2
by A68, ZFMISC_1:87;
hence h . (
0,
t) =
K1 . (
0,
t)
by A27, FUNCT_4:11
.=
f . (f1 . (0,t))
by A70, FUNCT_1:13
.=
f . (
(R1 . 0),
((id I[01]) . t))
by A71, FUNCT_3:65
.=
f . (
(R1 . 0),
t)
by FUNCT_1:18
.=
f . (
0,
t)
by Th33
.=
a
by A10
;
h . (1,t) = c
1
in [.(1 / 2),1.]
by XXREAL_1:1;
then A72:
1
in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then
1
in dom R2
by FUNCT_2:def 1;
then A73:
[1,t] in [:(dom R2),(dom (id I[01])):]
by ZFMISC_1:87;
1
in [.(1 / 2),1.]
by XXREAL_1:1;
then
1
in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then A74:
[1,t] in dom g1
by A8, ZFMISC_1:87;
[1,t] in dom K2
by A68, A72, ZFMISC_1:87;
then h . (1,
t) =
K2 . (1,
t)
by A27, FUNCT_4:13
.=
g . (g1 . (1,t))
by A74, FUNCT_1:13
.=
g . (
(R2 . 1),
((id I[01]) . t))
by A73, FUNCT_3:65
.=
g . (
(R2 . 1),
t)
by FUNCT_1:18
.=
g . (1,
t)
by Th33
.=
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 A28, A30; verum