let f, g be FinSequence of (TOP-REAL 2); ( f is being_S-Seq & g is being_S-Seq & ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) & L~ f misses L~ g & (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ f) = {(f /. (len f))} & (LSeg ((f /. (len f)),(g /. 1))) /\ (L~ g) = {(g /. 1)} implies f ^ g is being_S-Seq )
assume that
A1:
f is being_S-Seq
and
A2:
g is being_S-Seq
and
A3:
( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 )
and
A4:
L~ f misses L~ g
and
A5:
(LSeg ((f /. (len f)),(g /. 1))) /\ (L~ f) = {(f /. (len f))}
and
A6:
(LSeg ((f /. (len f)),(g /. 1))) /\ (L~ g) = {(g /. 1)}
; f ^ g is being_S-Seq
A7:
len g >= 2
by A2, TOPREAL1:def 8;
then A8:
len g >= 1
by XXREAL_0:2;
then
1 in dom g
by FINSEQ_3:25;
then A9:
g /. 1 in L~ g
by A7, GOBOARD1:1;
set h = <*(f /. (len f))*> ^ g;
A10:
len f >= 2
by A1, TOPREAL1:def 8;
then
1 <= len f
by XXREAL_0:2;
then A11:
len f in dom f
by FINSEQ_3:25;
then A12: f . (len f) =
f /. (len f)
by PARTFUN1:def 6
.=
(<*(f /. (len f))*> ^ g) . 1
by FINSEQ_1:41
;
A13: len (<*(f /. (len f))*> ^ g) =
(len <*(f /. (len f))*>) + (len g)
by FINSEQ_1:22
.=
(len g) + 1
by FINSEQ_1:39
;
then
len (<*(f /. (len f))*> ^ g) >= 1 + 1
by A8, XREAL_1:6;
then A14: mid ((<*(f /. (len f))*> ^ g),2,(len (<*(f /. (len f))*> ^ g))) =
((<*(f /. (len f))*> ^ g) /^ ((1 + 1) -' 1)) | (((len (<*(f /. (len f))*> ^ g)) -' 2) + 1)
by FINSEQ_6:def 3
.=
((<*(f /. (len f))*> ^ g) /^ 1) | (((len (<*(f /. (len f))*> ^ g)) -' 2) + 1)
by NAT_D:34
.=
g | (((len (<*(f /. (len f))*> ^ g)) -' 2) + 1)
by FINSEQ_6:45
.=
g | ((((len (<*(f /. (len f))*> ^ g)) -' 1) -' 1) + 1)
by NAT_D:45
.=
g | (((len g) -' 1) + 1)
by A13, NAT_D:34
.=
g | (len g)
by A7, XREAL_1:235, XXREAL_0:2
.=
g
by FINSEQ_1:58
;
f /. (len f) in L~ f
by A10, A11, GOBOARD1:1;
then
f /. (len f) <> g /. 1
by A4, A9, XBOOLE_0:3;
then A15:
<*(f /. (len f))*> ^ g is being_S-Seq
by A2, A3, A6, SPRECT_2:60;
(L~ f) /\ (L~ (<*(f /. (len f))*> ^ g)) =
(L~ f) /\ ((LSeg ((f /. (len f)),(g /. 1))) \/ (L~ g))
by A2, SPPOL_2:20
.=
((L~ f) /\ (LSeg ((f /. (len f)),(g /. 1)))) \/ ((L~ f) /\ (L~ g))
by XBOOLE_1:23
.=
((L~ f) /\ (LSeg ((f /. (len f)),(g /. 1)))) \/ {}
by A4
.=
{((<*(f /. (len f))*> ^ g) . 1)}
by A5, A11, A12, PARTFUN1:def 6
;
hence
f ^ g is being_S-Seq
by A1, A12, A15, A14, JORDAN3:38; verum