let f be constant standard special_circular_sequence; :: thesis:
let g be FinSequence of (TOP-REAL 2); :: thesis:
let i1, i2 be Nat; :: thesis:
assume that
A1: g is_a_part_of f,i1,i2 and
A2: g . 1 <> g . (len g) ; :: thesis:

now :: thesis:

per cases by A1;

case A3: g is_a_part>_of f,i1,i2 ; :: thesis:

then i1 + 1 <= len f ;
then A4: (i1 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
A5: 1 <= i1 by A3;
A6: 1 <= len g by A3;
len g < len f by A3;
then A7: i1 <= (len f) -' 1 by A6, A4, XREAL_1:233, XXREAL_0:2;

now :: thesis:

assume A8: i1 = i2 ; :: thesis:
g . 1 = f . (S_Drop (((i1 + 1) -' 1),f)) by A3
.= f . (S_Drop (i1,f)) by NAT_D:34
.= f . i1 by A5, A7, Th22 ;
hence contradiction by A2, A3, A8; :: thesis:

end;

hence L~ g is_S-P_arc_joining f /. i1,f /. i2 by A1, Th48; :: thesis:

end;

case A9: g is_a_part<_of f,i1,i2 ; :: thesis:

then A10: 1 <= i1 ;
A11: 1 <= len g by A9;
A12: len g < len f by A9;
i1 + 1 <= len f by A9;
then (i1 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
then A13: i1 <= (len f) -' 1 by A11, A12, XREAL_1:233, XXREAL_0:2;

now :: thesis:

assume A14: i1 = i2 ; :: thesis:
g . 1 = f . (S_Drop ((((len f) + i1) -' 1),f)) by A9
.= f . (S_Drop ((((((len f) -' 1) + 1) + i1) -' 1),f)) by A11, A12, XREAL_1:235, XXREAL_0:2
.= f . (S_Drop ((((((len f) -' 1) + i1) + 1) -' 1),f))
.= f . (S_Drop ((((len f) -' 1) + i1),f)) by NAT_D:34
.= f . (S_Drop (i1,f)) by Th23
.= f . i1 by A10, A13, Th22 ;
hence contradiction by A2, A9, A14; :: thesis:

end;

hence L~ g is_S-P_arc_joining f /. i1,f /. i2 by A1, Th48; :: thesis:

end;

end;

end;

hence L~ g is_S-P_arc_joining f /. i1,f /. i2 ; :: thesis: