let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( 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)} ; :: thesis: f ^ g is being_S-Seq
set h = <*(f /. (len f))*> ^ g;
A7: len f >= 2 by A1, TOPREAL1:def 10;
A8: len g >= 2 by A2, TOPREAL1:def 10;
1 <= len f by A7, XXREAL_0:2;
then A9: len f in dom f by FINSEQ_3:27;
A10: len g >= 1 by A8, XXREAL_0:2;
then A11: 1 in dom g by FINSEQ_3:27;
A12: len (<*(f /. (len f))*> ^ g) = (len <*(f /. (len f))*>) + (len g) by FINSEQ_1:35
.= (len g) + 1 by FINSEQ_1:56 ;
then A13: len (<*(f /. (len f))*> ^ g) >= 1 + 1 by A10, XREAL_1:8;
len g <> 0 by A2;
then A14: not g is empty ;
A15: f . (len f) = f /. (len f) by A9, PARTFUN1:def 8
.= (<*(f /. (len f))*> ^ g) . 1 by FINSEQ_1:58 ;
( f /. (len f) in L~ f & g /. 1 in L~ g ) by A7, A8, A9, A11, GOBOARD1:16;
then f /. (len f) <> g /. 1 by A4, XBOOLE_0:3;
then A16: <*(f /. (len f))*> ^ g is being_S-Seq by A2, A3, A6, SPRECT_2:64;
A17: (L~ f) /\ (L~ (<*(f /. (len f))*> ^ g)) = (L~ f) /\ ((LSeg (f /. (len f)),(g /. 1)) \/ (L~ g)) by A14, 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, XBOOLE_0:def 7
.= {((<*(f /. (len f))*> ^ g) . 1)} by A5, A9, A15, PARTFUN1:def 8 ;
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 A13, JORDAN3:def 1
.= ((<*(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:49
.= g | ((((len (<*(f /. (len f))*> ^ g)) -' 1) -' 1) + 1) by NAT_D:45
.= g | (((len g) -' 1) + 1) by A12, NAT_D:34
.= g | (len g) by A8, XREAL_1:237, XXREAL_0:2
.= g by FINSEQ_1:79 ;
hence f ^ g is being_S-Seq by A1, A15, A16, A17, JORDAN3:73; :: thesis: verum