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 & [s2,t2],[s3,t3] are_connected ) and
A2: p1 = pr1 l1 and
A3: p2 = pr1 l2 ; :: thesis: pr1 (l1 + l2) = p1 + p2
A4: ( s1,s2 are_connected & s2,s3 are_connected ) by A1, Th11;
now :: thesis: for x being Element of I[01] holds (pr1 (l1 + l2)) . x = (p1 + p2) . x
A5: dom l2 = the carrier of I[01] by FUNCT_2:def 1;
A6: dom l1 = the carrier of I[01] by FUNCT_2:def 1;
let x be Element of I[01]; :: thesis: (pr1 (l1 + l2)) . b1 = (p1 + p2) . b1
A7: dom (l1 + l2) = the carrier of I[01] by FUNCT_2:def 1;
per cases ( x <= 1 / 2 or x >= 1 / 2 ) ;
suppose A8: x <= 1 / 2 ; :: thesis: (pr1 (l1 + l2)) . b1 = (p1 + p2) . b1
then A9: 2 * x is Point of I[01] by BORSUK_6:3;
thus (pr1 (l1 + l2)) . x = ((l1 + l2) . x) `1 by A7, MCART_1:def 12
.= (l1 . (2 * x)) `1 by A1, A8, BORSUK_2:def 5
.= p1 . (2 * x) by A2, A6, A9, MCART_1:def 12
.= (p1 + p2) . x by A4, A8, BORSUK_2:def 5 ; :: thesis: verum
end;
suppose A10: x >= 1 / 2 ; :: thesis: (pr1 (l1 + l2)) . b1 = (p1 + p2) . b1
then A11: (2 * x) - 1 is Point of I[01] by BORSUK_6:4;
thus (pr1 (l1 + l2)) . x = ((l1 + l2) . x) `1 by A7, MCART_1:def 12
.= (l2 . ((2 * x) - 1)) `1 by A1, A10, BORSUK_2:def 5
.= p2 . ((2 * x) - 1) by A3, A5, A11, MCART_1:def 12
.= (p1 + p2) . x by A4, A10, BORSUK_2:def 5 ; :: thesis: verum
end;
end;
end;
hence pr1 (l1 + l2) = p1 + p2 ; :: thesis: verum