let S, T be non empty TopSpace; :: thesis: for s1, s2, s3 being Point of S
for t1, t2, t3 being Point of T
for l1 being Path of [s1,t1],[s2,t2]
for l2 being Path of [s2,t2],[s3,t3]
for p1 being Path of s1,s2
for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds
pr1 (l1 + l2) = p1 + p2
let s1, s2, s3 be Point of S; :: thesis: for t1, t2, t3 being Point of T
for l1 being Path of [s1,t1],[s2,t2]
for l2 being Path of [s2,t2],[s3,t3]
for p1 being Path of s1,s2
for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds
pr1 (l1 + l2) = p1 + p2
let t1, t2, t3 be Point of T; :: thesis: for l1 being Path of [s1,t1],[s2,t2]
for l2 being Path of [s2,t2],[s3,t3]
for p1 being Path of s1,s2
for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds
pr1 (l1 + l2) = p1 + p2
let l1 be Path of [s1,t1],[s2,t2]; :: thesis: for l2 being Path of [s2,t2],[s3,t3]
for p1 being Path of s1,s2
for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds
pr1 (l1 + l2) = p1 + p2
let l2 be Path of [s2,t2],[s3,t3]; :: thesis: for p1 being Path of s1,s2
for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds
pr1 (l1 + l2) = p1 + p2
let p1 be Path of s1,s2; :: thesis: for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 holds
pr1 (l1 + l2) = p1 + p2
let p2 be Path of s2,s3; :: thesis: ( [s1,t1],[s2,t2] are_connected & [s2,t2],[s3,t3] are_connected & p1 = pr1 l1 & p2 = pr1 l2 implies pr1 (l1 + l2) = p1 + p2 )
assume that
A1:
[s1,t1],[s2,t2] are_connected
and
A2:
[s2,t2],[s3,t3] are_connected
and
A3:
p1 = pr1 l1
and
A4:
p2 = pr1 l2
; :: thesis: pr1 (l1 + l2) = p1 + p2
A5:
s1,s2 are_connected
by A1, Th11;
A6:
s2,s3 are_connected
by A2, Th11;
now let x be
Element of
I[01] ;
:: thesis: (pr1 (l1 + l2)) . b1 = (p1 + p2) . b1A7:
dom (l1 + l2) = the
carrier of
I[01]
by FUNCT_2:def 1;
A8:
dom l1 = the
carrier of
I[01]
by FUNCT_2:def 1;
A9:
dom l2 = the
carrier of
I[01]
by FUNCT_2:def 1;
per cases
( x <= 1 / 2 or x >= 1 / 2 )
;
suppose A10:
x <= 1
/ 2
;
:: thesis: (pr1 (l1 + l2)) . b1 = (p1 + p2) . b1then A11:
2
* x is
Point of
I[01]
by BORSUK_6:6;
thus (pr1 (l1 + l2)) . x =
((l1 + l2) . x) `1
by A7, MCART_1:def 12
.=
(l1 . (2 * x)) `1
by A1, A2, A10, BORSUK_2:def 5
.=
p1 . (2 * x)
by A3, A8, A11, MCART_1:def 12
.=
(p1 + p2) . x
by A5, A6, A10, BORSUK_2:def 5
;
:: thesis: verum end; suppose A12:
x >= 1
/ 2
;
:: thesis: (pr1 (l1 + l2)) . b1 = (p1 + p2) . b1then A13:
(2 * x) - 1 is
Point of
I[01]
by BORSUK_6:7;
thus (pr1 (l1 + l2)) . x =
((l1 + l2) . x) `1
by A7, MCART_1:def 12
.=
(l2 . ((2 * x) - 1)) `1
by A1, A2, A12, BORSUK_2:def 5
.=
p2 . ((2 * x) - 1)
by A4, A9, A13, MCART_1:def 12
.=
(p1 + p2) . x
by A5, A6, A12, BORSUK_2:def 5
;
:: thesis: verum end; end;
hence
pr1 (l1 + l2) = p1 + p2
by FUNCT_2:113; :: thesis: verum