let f be non constant standard special_circular_sequence; :: thesis: for i, j being Element of 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 Element of 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, Th70;
A9: len (<*(NW-corner (L~ f))*> ^ (mid f,i,j)) = (len <*(NW-corner (L~ f))*>) + (len (mid f,i,j)) by FINSEQ_1:35;
len (mid f,i,j) in dom (mid f,i,j) by A3, FINSEQ_5:6;
then A10: (<*(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 A9, FINSEQ_4:84;
then A11: (<*(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, Th13;
then A12: (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:115;
A13: (LSeg (SE-corner (L~ f)),(S-max (L~ f))) /\ (L~ f) = {(S-max (L~ f))} by PSCOMP_1:122;
len (mid f,i,j) >= 2 by A3, TOPREAL1:def 10;
then A14: S-max (L~ f) in L~ (mid f,i,j) by A10, A11, JORDAN3:34;
A15: ( 1 <= i & i <= len f & 1 <= j & j <= len f ) by A1, A2, FINSEQ_3:27;
(mid f,i,j) /. 1 = f /. i by A1, A2, Th12;
then A16: 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;
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 A11, 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))) = {} by XBOOLE_0:def 7;
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 A16, XBOOLE_1:23
.= {((<*(NW-corner (L~ f))*> ^ (mid f,i,j)) /. (len (<*(NW-corner (L~ f))*> ^ (mid f,i,j))))} by A11, A13, A14, A15, JORDAN4:47, ZFMISC_1:150 ;
hence (<*(NW-corner (L~ f))*> ^ (mid f,i,j)) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2 by A7, A8, A11, A12, Th65; :: thesis: verum