let g1 be FinSequence of (TOP-REAL 2); :: thesis: for i being Nat st 1 <= i & i <= len g1 & g1 is being_S-Seq & g1 /. 1 in L~ (mid (g1,i,(len g1))) holds
i = 1
let i be Nat; :: thesis: ( 1 <= i & i <= len g1 & g1 is being_S-Seq & g1 /. 1 in L~ (mid (g1,i,(len g1))) implies i = 1 )
assume that
A1: 1 <= i and
A2: i <= len g1 and
A3: g1 is being_S-Seq ; :: thesis: ( not g1 /. 1 in L~ (mid (g1,i,(len g1))) or i = 1 )
assume g1 /. 1 in L~ (mid (g1,i,(len g1))) ; :: thesis: i = 1
then consider j being Nat such that
A4: 1 <= j and
A5: j + 1 <= len (mid (g1,i,(len g1))) and
A6: g1 /. 1 in LSeg ((mid (g1,i,(len g1))),j) by SPPOL_2:13;
A7: j + 1 in dom (mid (g1,i,(len g1))) by A4, A5, SEQ_4:134;
A8: mid (g1,i,(len g1)) = g1 /^ (i -' 1) by A2, FINSEQ_6:117;
j <= j + 1 by NAT_1:11;
then A9: j <= len (g1 /^ (i -' 1)) by A5, A8, XXREAL_0:2;
then A10: j in dom (g1 /^ (i -' 1)) by A4, FINSEQ_3:25;
i -' 1 <= i by A1, Th1;
then A11: i -' 1 <= len g1 by A2, XXREAL_0:2;
then A12: j <= (len g1) - (i -' 1) by A9, RFINSEQ:def 1;
j <= (i -' 1) + j by NAT_1:11;
then A13: 1 <= (i -' 1) + j by A4, XXREAL_0:2;
A14: j + (i -' 1) <= len g1 by A12, XREAL_1:19;
then A15: (i -' 1) + j in dom g1 by A13, FINSEQ_3:25;
A16: (g1 /^ (i -' 1)) /. j = (g1 /^ (i -' 1)) . j by A10, PARTFUN1:def 6
.= g1 . ((i -' 1) + j) by A4, A14, FINSEQ_6:114
.= g1 /. ((i -' 1) + j) by A15, PARTFUN1:def 6 ;
A17: 1 <= j + 1 by NAT_1:11;
j + 1 <= (i -' 1) + (j + 1) by NAT_1:11;
then A18: 1 <= (i -' 1) + (j + 1) by A17, XXREAL_0:2;
j + 1 <= len (g1 /^ (i -' 1)) by A2, A5, FINSEQ_6:117;
then A19: j + 1 <= (len g1) - (i -' 1) by A11, RFINSEQ:def 1;
A20: 1 <= j + 1 by A7, FINSEQ_3:25;
A21: (j + 1) + (i -' 1) <= len g1 by A19, XREAL_1:19;
then A22: (i -' 1) + (j + 1) in dom g1 by A18, FINSEQ_3:25;
j + 1 in dom (g1 /^ (i -' 1)) by A2, A7, FINSEQ_6:117;
then A23: (g1 /^ (i -' 1)) /. (j + 1) = (g1 /^ (i -' 1)) . (j + 1) by PARTFUN1:def 6
.= g1 . ((i -' 1) + (j + 1)) by A20, A21, FINSEQ_6:114
.= g1 /. ((i -' 1) + (j + 1)) by A22, PARTFUN1:def 6 ;
A24: ((i -' 1) + j) + 1 = (i -' 1) + (j + 1) ;
A25: ((i -' 1) + j) + 1 <= len g1 by A21;
A26: LSeg ((mid (g1,i,(len g1))),j) = LSeg ((g1 /. ((i -' 1) + j)),(g1 /. ((i -' 1) + (j + 1)))) by A4, A5, A8, A16, A23, TOPREAL1:def 3
.= LSeg (g1,((i -' 1) + j)) by A13, A21, A24, TOPREAL1:def 3 ;
A27: 1 + 1 <= len g1 by A3, TOPREAL1:def 8;
then g1 /. 1 in LSeg (g1,1) by TOPREAL1:21;
then A28: g1 /. 1 in (LSeg (g1,1)) /\ (LSeg (g1,((i -' 1) + j))) by A6, A26, XBOOLE_0:def 4;
then A29: LSeg (g1,1) meets LSeg (g1,((i -' 1) + j)) ;
assume i <> 1 ; :: thesis: contradiction
then 1 < i by A1, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then 2 -' 1 <= i -' 1 by NAT_D:42;
then (2 -' 1) + 1 <= (i -' 1) + j by A4, XREAL_1:7;
then A30: (i -' 1) + j >= 2 by XREAL_1:235;
A31: ( g1 is s.n.c. & g1 is unfolded & g1 is one-to-one ) by A3;
A32: 1 in dom g1 by A27, SEQ_4:134;
A33: 1 + 1 in dom g1 by A27, SEQ_4:134;

per cases ( (i -' 1) + j = 2 or (i -' 1) + j > 2 ) by A30, XXREAL_0:1;

suppose (i -' 1) + j = 2 ; :: thesis: contradiction

then g1 /. 1 in {(g1 /. (1 + 1))} by A25, A28, A31, TOPREAL1:def 6;
then g1 /. 1 = g1 /. (1 + 1) by TARSKI:def 1;
hence contradiction by A31, A32, A33, PARTFUN2:10; :: thesis: verum

end;

suppose (i -' 1) + j > 2 ; :: thesis: contradiction

then (i -' 1) + j > 1 + 1 ;
hence contradiction by A29, A31, TOPREAL1:def 7; :: thesis: verum

end;

end;