let T be non empty TopSpace; :: thesis: for a, b, c being Point of T

for G1 being Path of a,b

for G2 being Path of b,c st G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c holds

( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c )

let a, b, c be Point of T; :: thesis: for G1 being Path of a,b

for G2 being Path of b,c st G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c holds

( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c )

let G1 be Path of a,b; :: thesis: for G2 being Path of b,c st G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c holds

( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c )

let G2 be Path of b,c; :: thesis: ( G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c implies ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c ) )

assume ( G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c ) ; :: thesis: ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c )

then ex h being Function of I[01],T st

( h is continuous & h . 0 = a & h . 1 = c & rng h c= (rng G1) \/ (rng G2) ) by Lm3;

then a,c are_connected ;

hence ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c ) by Def2; :: thesis: verum

for G1 being Path of a,b

for G2 being Path of b,c st G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c holds

( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c )

let a, b, c be Point of T; :: thesis: for G1 being Path of a,b

for G2 being Path of b,c st G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c holds

( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c )

let G1 be Path of a,b; :: thesis: for G2 being Path of b,c st G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c holds

( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c )

let G2 be Path of b,c; :: thesis: ( G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c implies ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c ) )

assume ( G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c ) ; :: thesis: ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c )

then ex h being Function of I[01],T st

( h is continuous & h . 0 = a & h . 1 = c & rng h c= (rng G1) \/ (rng G2) ) by Lm3;

then a,c are_connected ;

hence ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c ) by Def2; :: thesis: verum