let T be non empty TopSpace; for c1, c2 being with_endpoints Curve of T st sup (dom c1) = inf (dom c2) & the_last_point_of c1 = the_first_point_of c2 holds
( c1 + c2 is with_endpoints & dom (c1 + c2) = [.(inf (dom c1)),(sup (dom c2)).] & (c1 + c2) . (inf (dom c1)) = the_first_point_of c1 & (c1 + c2) . (sup (dom c2)) = the_last_point_of c2 )
let c1, c2 be with_endpoints Curve of T; ( sup (dom c1) = inf (dom c2) & the_last_point_of c1 = the_first_point_of c2 implies ( c1 + c2 is with_endpoints & dom (c1 + c2) = [.(inf (dom c1)),(sup (dom c2)).] & (c1 + c2) . (inf (dom c1)) = the_first_point_of c1 & (c1 + c2) . (sup (dom c2)) = the_last_point_of c2 ) )
assume A1:
sup (dom c1) = inf (dom c2)
; ( not the_last_point_of c1 = the_first_point_of c2 or ( c1 + c2 is with_endpoints & dom (c1 + c2) = [.(inf (dom c1)),(sup (dom c2)).] & (c1 + c2) . (inf (dom c1)) = the_first_point_of c1 & (c1 + c2) . (sup (dom c2)) = the_last_point_of c2 ) )
assume A2:
the_last_point_of c1 = the_first_point_of c2
; ( c1 + c2 is with_endpoints & dom (c1 + c2) = [.(inf (dom c1)),(sup (dom c2)).] & (c1 + c2) . (inf (dom c1)) = the_first_point_of c1 & (c1 + c2) . (sup (dom c2)) = the_last_point_of c2 )
set f = c1 \/ c2;
A3:
dom (c1 \/ c2) = (dom c1) \/ (dom c2)
by XTUPLE_0:23;
reconsider f1 = c1 as parametrized-curve PartFunc of R^1,T by Th23;
A4:
dom f1 is interval Subset of REAL
by Def4;
reconsider f2 = c2 as parametrized-curve PartFunc of R^1,T by Th23;
A5:
dom f2 is interval Subset of REAL
by Def4;
A6:
(dom c1) \/ (dom c2) c= REAL
by A4, A5, XBOOLE_1:8;
( rng f1 c= [#] T & rng f2 c= [#] T )
;
then
(rng c1) \/ (rng c2) c= [#] T
by XBOOLE_1:8;
then A7:
rng (c1 \/ c2) c= [#] T
by RELAT_1:12;
A8:
dom (c1 \/ c2) c= [#] R^1
by A6, TOPMETR:17, XTUPLE_0:23;
reconsider S0 = dom (c1 \/ c2) as Subset of R^1 by A6, TOPMETR:17, XTUPLE_0:23;
A9:
inf (dom c2) <= sup (dom c2)
by XXREAL_2:40;
A10:
inf (dom c1) <= sup (dom c1)
by XXREAL_2:40;
A11:
dom f1 = [.(inf (dom c1)),(sup (dom c1)).]
by Th27;
A12:
dom f2 = [.(inf (dom c2)),(sup (dom c2)).]
by Th27;
A13:
(dom f1) /\ (dom f2) = {(sup (dom c1))}
by A11, A12, A1, A9, A10, XXREAL_1:418;
A14:
(dom f1) /\ (dom f2) c= dom (c1 \/ c2)
by A3, XBOOLE_1:29;
set S = R^1 | S0;
consider S1 being SubSpace of R^1 , g1 being Function of S1,T such that
A15:
( f1 = g1 & S1 = R^1 | (dom f1) & g1 is continuous )
by Def4;
consider S2 being SubSpace of R^1 , g2 being Function of S2,T such that
A16:
( f2 = g2 & S2 = R^1 | (dom f2) & g2 is continuous )
by Def4;
sup (dom c1) in dom (c1 \/ c2)
by A13, A14, ZFMISC_1:31;
then
sup (dom c1) in [#] (R^1 | S0)
by PRE_TOPC:def 5;
then reconsider p = sup (dom c1) as Point of (R^1 | S0) ;
reconsider S1 = S1, S2 = S2 as SubSpace of R^1 | S0 by A15, A16, A3, TOPMETR:22, XBOOLE_1:7;
A17: ([#] S1) \/ ([#] S2) =
(dom f1) \/ ([#] S2)
by A15, PRE_TOPC:def 5
.=
(dom f1) \/ (dom f2)
by A16, PRE_TOPC:def 5
.=
[#] (R^1 | S0)
by A3, PRE_TOPC:def 5
;
A18: ([#] S1) /\ ([#] S2) =
(dom f1) /\ ([#] S2)
by A15, PRE_TOPC:def 5
.=
{p}
by A13, A16, PRE_TOPC:def 5
;
S1 = Closed-Interval-TSpace ((inf (dom c1)),(sup (dom c1)))
by A11, A10, A15, TOPMETR:19;
then A19:
S1 is compact
by A10, HEINE:4;
S2 = Closed-Interval-TSpace ((inf (dom c2)),(sup (dom c2)))
by A12, A9, A16, TOPMETR:19;
then A20:
S2 is compact
by A9, HEINE:4;
A21:
R^1 | S0 is T_2
by TOPMETR:2;
A22:
g1 +* g2 is continuous Function of (R^1 | S0),T
by A17, A18, A19, A20, A21, A15, A16, A1, A2, COMPTS_1:20;
for x, y1, y2 being object st [x,y1] in c1 \/ c2 & [x,y2] in c1 \/ c2 holds
y1 = y2
then reconsider f = c1 \/ c2 as Function by FUNCT_1:def 1;
A26:
dom f = (dom g1) \/ (dom g2)
by A15, A16, XTUPLE_0:23;
for x being object st x in (dom g1) \/ (dom g2) holds
( ( x in dom g2 implies f . x = g2 . x ) & ( not x in dom g2 implies f . x = g1 . x ) )
then A28:
f = g1 +* g2
by A26, FUNCT_4:def 1;
reconsider f = f as PartFunc of R^1,T by A7, A8, RELSET_1:4;
dom c1 meets dom c2
by A13;
then
dom f is interval Subset of REAL
by A4, A5, A3, XBOOLE_1:8, XXREAL_2:89;
then
f is parametrized-curve
by A22, A28;
then A29:
c1 \/ c2 is Curve of T
by Th20;
then A30:
c1 + c2 = c1 \/ c2
by Def12;
A31:
dom (c1 \/ c2) = [.(inf (dom c1)),(sup (dom c2)).]
by A3, A11, A12, A1, A9, A10, XXREAL_1:165;
A32:
inf (dom c1) in dom f1
by A11, A10, XXREAL_1:1;
then
inf (dom c1) in dom f
by A3, XBOOLE_0:def 3;
then
inf (dom f) in dom f
by A31, A1, A9, A10, XXREAL_0:2, XXREAL_2:25;
then
dom (c1 + c2) is left_end
by A30, XXREAL_2:def 5;
then A33:
c1 + c2 is with_first_point
;
A34:
sup (dom c2) in dom f2
by A12, A9, XXREAL_1:1;
then
sup (dom c2) in dom f
by A3, XBOOLE_0:def 3;
then
sup [.(inf (dom c1)),(sup (dom c2)).] in dom f
by A1, A9, A10, XXREAL_0:2, XXREAL_2:29;
then
dom (c1 + c2) is right_end
by A31, A30, XXREAL_2:def 6;
then A35:
c1 + c2 is with_last_point
;
thus
( c1 + c2 is with_endpoints & dom (c1 + c2) = [.(inf (dom c1)),(sup (dom c2)).] )
by A33, A35, A30, A3, A11, A12, A1, A9, A10, XXREAL_1:165; ( (c1 + c2) . (inf (dom c1)) = the_first_point_of c1 & (c1 + c2) . (sup (dom c2)) = the_last_point_of c2 )
A36:
(c1 + c2) . (inf (dom c1)) = c1 . (inf (dom c1))
thus
(c1 + c2) . (inf (dom c1)) = the_first_point_of c1
by A36; (c1 + c2) . (sup (dom c2)) = the_last_point_of c2
A38:
(c1 + c2) . (sup (dom c2)) = c2 . (sup (dom c2))
thus
(c1 + c2) . (sup (dom c2)) = the_last_point_of c2
by A38; verum