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 & i1 < i2 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 & i1 < i2 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 & i1 < i2 implies L~ g is_S-P_arc_joining f /. i1,f /. i2 )
assume A1: ( g is_a_part>_of f,i1,i2 & i1 < i2 ) ; :: thesis: L~ g is_S-P_arc_joining f /. i1,f /. i2
then A2: ( len g = (i2 -' i1) + 1 & g = mid f,i1,i2 ) by Th37;
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 A1, Def2;
then A4: g is being_S-Seq by A1, A2, Th51;
A5: i1 < len f by A3, NAT_1:13;
A6: i2 < len f by A3, NAT_1:13;
then A7: g . 1 = f . i1 by A2, A3, A5, JORDAN3:27;
A8: f /. i1 = f . i1 by A3, A5, FINSEQ_4:24;
g /. (len g) = g . (len g) by A3, FINSEQ_4:24;
then ( f /. i1 = g /. 1 & f /. i2 = g /. (len g) ) by A3, A6, A7, A8, FINSEQ_4:24;
hence L~ g is_S-P_arc_joining f /. i1,f /. i2 by A4, TOPREAL4:def 1; :: thesis: verum