let g1 be FinSequence of (TOP-REAL 2); :: thesis: for i being Element of 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 Element of 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 Element of 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, GOBOARD2:3;
A8: mid g1,i,(len g1) = g1 /^ (i -' 1) by A2, JORDAN3:26;
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:27;
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 2;
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:21;
then A15: (i -' 1) + j in dom g1 by A13, FINSEQ_3:27;
A16: (g1 /^ (i -' 1)) /. j = (g1 /^ (i -' 1)) . j by A10, PARTFUN1:def 8
.= g1 . ((i -' 1) + j) by A4, A14, JORDAN3:23
.= g1 /. ((i -' 1) + j) by A15, PARTFUN1:def 8 ;
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, JORDAN3:26;
then A19: j + 1 <= (len g1) - (i -' 1) by A11, RFINSEQ:def 2;
A20: 1 <= j + 1 by A7, FINSEQ_3:27;
A21: (j + 1) + (i -' 1) <= len g1 by A19, XREAL_1:21;
then A22: (i -' 1) + (j + 1) in dom g1 by A18, FINSEQ_3:27;
j + 1 in dom (g1 /^ (i -' 1)) by A2, A7, JORDAN3:26;
then A23: (g1 /^ (i -' 1)) /. (j + 1) = (g1 /^ (i -' 1)) . (j + 1) by PARTFUN1:def 8
.= g1 . ((i -' 1) + (j + 1)) by A20, A21, JORDAN3:23
.= g1 /. ((i -' 1) + (j + 1)) by A22, PARTFUN1:def 8 ;
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 5
.= LSeg g1,((i -' 1) + j) by A13, A21, A24, TOPREAL1:def 5 ;
A27: 1 + 1 <= len g1 by A3, TOPREAL1:def 10;
then g1 /. 1 in LSeg g1,1 by TOPREAL1:27;
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) by XBOOLE_0:4;
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:9;
then A30: (i -' 1) + j >= 2 by XREAL_1:237;
A31: ( g1 is s.n.c. & g1 is unfolded & g1 is one-to-one ) by A3, TOPREAL1:def 10;
A32: 1 in dom g1 by A27, GOBOARD2:3;
A33: 1 + 1 in dom g1 by A27, GOBOARD2:3;

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 8;
then g1 /. 1 = g1 /. (1 + 1) by TARSKI:def 1;
hence contradiction by A31, A32, A33, PARTFUN2:17; :: thesis: verum

end;

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

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

end;

end;