let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( not f is empty & not g is trivial & f /. (len f) = g /. 1 implies L~ (f ^' g) = (L~ f) \/ (L~ g) )
assume that
A1: not f is empty and
A2: not g is trivial and
A3: f /. (len f) = g /. 1 ; :: thesis: L~ (f ^' g) = (L~ f) \/ (L~ g)
set c = (1 + 1),(len g) -cut g;
A4: (1 + 1),(len g) -cut g = g /^ 1 by Th13;
A5: len g > 1 by A2, Th2;
then len ((1 + 1),(len g) -cut g) = (len g) - 1 by A4, RFINSEQ:def 2;
then len ((1 + 1),(len g) -cut g) > 1 - 1 by A5, XREAL_1:11;
then A6: not (1 + 1),(len g) -cut g is empty ;

now

assume g is empty ; :: thesis: contradiction
then g = <*> the carrier of (TOP-REAL 2) ;
hence contradiction by A4, A6, FINSEQ_6:86; :: thesis: verum

end;

then g = <*(g /. 1)*> ^ ((1 + 1),(len g) -cut g) by A4, FINSEQ_5:32;
then A7: (LSeg (g /. 1),(((1 + 1),(len g) -cut g) /. 1)) \/ (L~ ((1 + 1),(len g) -cut g)) = L~ g by A6, SPPOL_2:20;
L~ (f ^ ((1 + 1),(len g) -cut g)) = ((L~ f) \/ (LSeg (f /. (len f)),(((1 + 1),(len g) -cut g) /. 1))) \/ (L~ ((1 + 1),(len g) -cut g)) by A1, A6, SPPOL_2:23
.= (L~ f) \/ ((LSeg (g /. 1),(((1 + 1),(len g) -cut g) /. 1)) \/ (L~ ((1 + 1),(len g) -cut g))) by A3, XBOOLE_1:4 ;
hence L~ (f ^' g) = (L~ f) \/ (L~ g) by A7, GRAPH_2:def 2; :: thesis: verum