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