let f be non constant standard special_circular_sequence; :: thesis: for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part_of f,i1,i2 & g . 1 <> g . (len g) holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
let g be FinSequence of (TOP-REAL 2); :: thesis: for i1, i2 being Element of NAT st g is_a_part_of f,i1,i2 & g . 1 <> g . (len g) holds
L~ g is_S-P_arc_joining f /. i1,f /. i2
let i1, i2 be Element of NAT ; :: thesis: ( g is_a_part_of f,i1,i2 & g . 1 <> g . (len g) implies L~ g is_S-P_arc_joining f /. i1,f /. i2 )
assume A1: ( g is_a_part_of f,i1,i2 & g . 1 <> g . (len g) ) ; :: thesis: L~ g is_S-P_arc_joining f /. i1,f /. i2

now

per cases ( g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2 ) by A1, Def4;

case A2: g is_a_part>_of f,i1,i2 ; :: thesis: L~ g is_S-P_arc_joining f /. i1,f /. i2

then A3: ( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & g . (len g) = f . i2 & 1 <= len g & len g < len f & ( for i being Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) ) ) by Def2;
then A4: 1 < len f by XXREAL_0:2;
(i1 + 1) - 1 <= (len f) - 1 by A3, XREAL_1:11;
then A5: i1 <= (len f) -' 1 by A4, XREAL_1:235;

now

assume A6: i1 = i2 ; :: thesis: contradiction
g . 1 = f . (S_Drop ((i1 + 1) -' 1),f) by A3
.= f . (S_Drop i1,f) by NAT_D:34
.= f . i1 by A3, A5, Th34 ;
hence contradiction by A1, A2, A6, Def2; :: thesis: verum

end;

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

end;

case A7: g is_a_part<_of f,i1,i2 ; :: thesis: L~ g is_S-P_arc_joining f /. i1,f /. i2

then A8: ( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & g . (len g) = f . i2 & 1 <= len g & len g < len f & ( for i being Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((len f) + i1) -' i),f) ) ) by Def3;
then A9: 1 < len f by XXREAL_0:2;
(i1 + 1) - 1 <= (len f) - 1 by A8, XREAL_1:11;
then A10: i1 <= (len f) -' 1 by A9, XREAL_1:235;

now

assume A11: i1 = i2 ; :: thesis: contradiction
g . 1 = f . (S_Drop (((len f) + i1) -' 1),f) by A8
.= f . (S_Drop (((((len f) -' 1) + 1) + i1) -' 1),f) by A9, XREAL_1:237
.= 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 Th35
.= f . i1 by A8, A10, Th34 ;
hence contradiction by A1, A7, A11, Def3; :: thesis: verum

end;

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

end;

end;

end;

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