let f, g be FinSequence of (TOP-REAL 2); ( 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
; 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 1;
then
len (((1 + 1),(len g)) -cut g) > 1 - 1
by A5, XREAL_1:9;
then
len (((1 + 1),(len g)) -cut g) > 0
;
then A6:
not ((1 + 1),(len g)) -cut g is empty
;
not g is empty
by A2;
then
g = <*(g /. 1)*> ^ (((1 + 1),(len g)) -cut g)
by A4, FINSEQ_5:29;
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, FINSEQ_6:def 5; verum