let f be constant standard special_circular_sequence; :: thesis: for g being FinSequence of (TOP-REAL 2)
for i1, i2 being 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 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 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 that
A1: g is_a_part>_of f,i1,i2 and
A2: i1 < i2 ; :: thesis: L~ g is_S-P_arc_joining f /. i1,f /. i2
A3: 1 <= i1 by A1;
i1 + 1 <= len f by A1;
then A4: i1 < len f by NAT_1:13;
then A5: f /. i1 = f . i1 by A3, FINSEQ_4:15;
A6: i2 + 1 <= len f by A1;
then A7: i2 < len f by NAT_1:13;
A8: 1 <= len g by A1;
then A9: g /. (len g) = g . (len g) by FINSEQ_4:15;
A10: 1 <= i2 by A1;
A11: g = mid (f,i1,i2) by A1, A2, Th25;
then g . 1 = f . i1 by A3, A10, A4, A7, FINSEQ_6:118;
then A12: f /. i1 = g /. 1 by A8, A5, FINSEQ_4:15;
g . (len g) = f . i2 by A1;
then A13: f /. i2 = g /. (len g) by A10, A7, A9, FINSEQ_4:15;
g is being_S-Seq by A2, A11, A3, A6, Th39;
hence L~ g is_S-P_arc_joining f /. i1,f /. i2 by A12, A13, TOPREAL4:def 1; :: thesis: verum