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

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
end;

hence
( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )
by Def12; :: thesis: verumper cases
( r < inf (dom c) or r >= inf (dom c) )
;

end;

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;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

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

end;

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

end;