let T be non empty TopStruct ; :: thesis: for c being with_endpoints Curve of T
for r being Real ex c1, c2 being Element of Curves T st
( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )
let c be with_endpoints Curve of T; :: thesis: for r being Real ex c1, c2 being Element of Curves T st
( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )
let r be Real; :: thesis: ex c1, c2 being Element of Curves T st
( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )
set c1 = c | [.(inf (dom c)),r.];
set c2 = c | [.r,(sup (dom c)).];
reconsider c1 = c | [.(inf (dom c)),r.] as Curve of T by Th26;
reconsider c2 = c | [.r,(sup (dom c)).] as Curve of T by Th26;
take c1 ; :: thesis: ex c2 being Element of Curves T st
( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )
take c2 ; :: thesis: ( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )
c1 \/ c2 = c

proof

per cases ( r < inf (dom c) or r >= inf (dom c) ) ;

suppose A1: r < inf (dom c) ; :: thesis: c1 \/ c2 = c

then [.(inf (dom c)),r.] = {} by XXREAL_1:29;
then A2: c1 = {} ;
[.(inf (dom c)),(sup (dom c)).] c= [.r,(sup (dom c)).] by A1, XXREAL_1:34;
then dom c c= [.r,(sup (dom c)).] by Th27;
hence c1 \/ c2 = c by A2, RELAT_1:68; :: thesis: verum

end;

suppose A3: r >= inf (dom c) ; :: thesis: c1 \/ c2 = c

per cases ( r > sup (dom c) or r <= sup (dom c) ) ;

suppose A4: r > sup (dom c) ; :: thesis: c1 \/ c2 = c

then [.r,(sup (dom c)).] = {} by XXREAL_1:29;
then A5: c2 = {} ;
[.(inf (dom c)),(sup (dom c)).] c= [.(inf (dom c)),r.] by A4, XXREAL_1:34;
then dom c c= [.(inf (dom c)),r.] by Th27;
hence c1 \/ c2 = c by A5, RELAT_1:68; :: thesis: verum

end;

suppose A6: r <= sup (dom c) ; :: thesis: c1 \/ c2 = c

dom c = [.(inf (dom c)),(sup (dom c)).] by Th27
.= [.(inf (dom c)),r.] \/ [.r,(sup (dom c)).] by A6, A3, XXREAL_1:165 ;
then c | (dom c) = c1 \/ c2 by RELAT_1:78;
hence c1 \/ c2 = c ; :: thesis: verum

end;

end;

end;

end;

end;

hence ( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] ) by Def12; :: thesis: verum