let f be V22() standard special_circular_sequence; 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; ( 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)
; (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; verum