let f be constant standard special_circular_sequence; :: thesis: for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. i = N-min (L~ f) & N-min (L~ f) <> NW-corner (L~ f) & f /. j = S-max (L~ f) & S-max (L~ f) <> SE-corner (L~ f) holds
(<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2
set p = NW-corner (L~ f);
set q = SE-corner (L~ f);
let i, j be Nat; :: thesis: ( i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. i = N-min (L~ f) & N-min (L~ f) <> NW-corner (L~ f) & f /. j = S-max (L~ f) & S-max (L~ f) <> SE-corner (L~ f) implies (<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2 )
assume that
A1: i in dom f and
A2: j in dom f and
A3: mid (f,i,j) is S-Sequence_in_R2 and
A4: f /. i = N-min (L~ f) and
A5: N-min (L~ f) <> NW-corner (L~ f) and
A6: f /. j = S-max (L~ f) and
A7: S-max (L~ f) <> SE-corner (L~ f) ; :: thesis: (<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2
set g = <*(NW-corner (L~ f))*> ^ (mid (f,i,j));
A8: <*(NW-corner (L~ f))*> ^ (mid (f,i,j)) is S-Sequence_in_R2 by A1, A2, A3, A4, A5, Th66;
( len (<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) = (len <*(NW-corner (L~ f))*>) + (len (mid (f,i,j))) & len (mid (f,i,j)) in dom (mid (f,i,j)) ) by A3, FINSEQ_1:22, FINSEQ_5:6;
then A9: (<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) /. (len (<*(NW-corner (L~ f))*> ^ (mid (f,i,j)))) = (mid (f,i,j)) /. (len (mid (f,i,j))) by FINSEQ_4:69;
then A10: (<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) /. (len (<*(NW-corner (L~ f))*> ^ (mid (f,i,j)))) = S-max (L~ f) by A1, A2, A6, Th9;
then A11: (SE-corner (L~ f)) `2 = ((<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) /. (len (<*(NW-corner (L~ f))*> ^ (mid (f,i,j))))) `2 by PSCOMP_1:53;
(mid (f,i,j)) /. 1 = f /. i by A1, A2, Th8;
then A12: L~ (<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) = (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) \/ (L~ (mid (f,i,j))) by A3, A4, SPPOL_2:20;
A13: ( 1 <= j & j <= len f ) by A2, FINSEQ_3:25;
A14: ( 1 <= i & i <= len f ) by A1, FINSEQ_3:25;
len (mid (f,i,j)) >= 2 by A3, TOPREAL1:def 8;
then A15: ( (LSeg ((SE-corner (L~ f)),(S-max (L~ f)))) /\ (L~ f) = {(S-max (L~ f))} & S-max (L~ f) in L~ (mid (f,i,j)) ) by A9, A10, JORDAN3:1, PSCOMP_1:59;
LSeg (((<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) /. (len (<*(NW-corner (L~ f))*> ^ (mid (f,i,j))))),(SE-corner (L~ f))) misses LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A10, Lm2;
then (LSeg ((SE-corner (L~ f)),((<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) /. (len (<*(NW-corner (L~ f))*> ^ (mid (f,i,j))))))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) = {} ;
then (LSeg ((SE-corner (L~ f)),((<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) /. (len (<*(NW-corner (L~ f))*> ^ (mid (f,i,j))))))) /\ (L~ (<*(NW-corner (L~ f))*> ^ (mid (f,i,j)))) = ((LSeg ((SE-corner (L~ f)),((<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) /. (len (<*(NW-corner (L~ f))*> ^ (mid (f,i,j))))))) /\ (L~ (mid (f,i,j)))) \/ {} by A12, XBOOLE_1:23
.= {((<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) /. (len (<*(NW-corner (L~ f))*> ^ (mid (f,i,j)))))} by A10, A15, A14, A13, JORDAN4:35, ZFMISC_1:124 ;
hence (<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2 by A7, A8, A10, A11, Th61; :: thesis: verum