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 /. j = N-max (L~ f) & N-max (L~ f) <> NE-corner (L~ f) holds
(mid (f,i,j)) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2
set p = NE-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 /. j = N-max (L~ f) & N-max (L~ f) <> NE-corner (L~ f) implies (mid (f,i,j)) ^ <*(NE-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 /. j = N-max (L~ f) and
A5: N-max (L~ f) <> NE-corner (L~ f) ; :: thesis: (mid (f,i,j)) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2
A6: ( 1 <= i & i <= len f ) by A1, FINSEQ_3:25;
A7: (mid (f,i,j)) /. (len (mid (f,i,j))) = N-max (L~ f) by A1, A2, A4, Th9;
then A8: (NE-corner (L~ f)) `2 = ((mid (f,i,j)) /. (len (mid (f,i,j)))) `2 by PSCOMP_1:37;
A9: ( 1 <= j & j <= len f ) by A2, FINSEQ_3:25;
len (mid (f,i,j)) >= 2 by A3, TOPREAL1:def 8;
then ( (LSeg ((NE-corner (L~ f)),(N-max (L~ f)))) /\ (L~ f) = {(N-max (L~ f))} & N-max (L~ f) in L~ (mid (f,i,j)) ) by A7, JORDAN3:1, PSCOMP_1:43;
then (LSeg ((NE-corner (L~ f)),((mid (f,i,j)) /. (len (mid (f,i,j)))))) /\ (L~ (mid (f,i,j))) = {((mid (f,i,j)) /. (len (mid (f,i,j))))} by A7, A6, A9, JORDAN4:35, ZFMISC_1:124;
hence (mid (f,i,j)) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2 by A3, A5, A7, A8, Th61; :: thesis: verum