let X be Path of a,c; :: thesis: ( X = P + Q iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies X . t = P . (2 * t) ) & ( 1 / 2 <= t implies X . t = Q . ((2 * t) - 1) ) ) )
( a,b are_connected & b,c are_connected ) by BORSUK_2:def 3;
hence ( X = P + Q iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies X . t = P . (2 * t) ) & ( 1 / 2 <= t implies X . t = Q . ((2 * t) - 1) ) ) ) by BORSUK_2:def 5; :: thesis: verum