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 /. j = S-max (L~ f) & S-max (L~ f) <> SE-corner (L~ f) holds
(mid f,i,j) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2
set p = 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 /. j = S-max (L~ f) & S-max (L~ f) <> SE-corner (L~ f) implies (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 /. j = S-max (L~ f) and
A5: S-max (L~ f) <> SE-corner (L~ f) ; :: thesis: (mid f,i,j) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2
A6: (mid f,i,j) /. (len (mid f,i,j)) = S-max (L~ f) by A1, A2, A4, Th13;
then A7: (SE-corner (L~ f)) `2 = ((mid f,i,j) /. (len (mid f,i,j))) `2 by PSCOMP_1:115;
A8: (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 A9: S-max (L~ f) in L~ (mid f,i,j) by A6, JORDAN3:34;
( 1 <= i & i <= len f & 1 <= j & j <= len f ) by A1, A2, FINSEQ_3:27;
then (LSeg (SE-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 A6, A8, A9, JORDAN4:47, ZFMISC_1:150;
hence (mid f,i,j) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2 by A3, A5, A6, A7, Th65; :: thesis: verum