let f be constant standard special_circular_sequence; :: thesis: for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 < len f holds
mid (f,i2,i1) is_a_part<_of f,i2,i1
let i1, i2 be Nat; :: thesis: ( 1 <= i1 & i1 <= i2 & i2 < len f implies mid (f,i2,i1) is_a_part<_of f,i2,i1 )
assume that
A1: 1 <= i1 and
A2: i1 <= i2 and
A3: i2 < len f ; :: thesis: mid (f,i2,i1) is_a_part<_of f,i2,i1
Rev (mid (f,i1,i2)) is_a_part<_of f,i2,i1 by A1, A2, A3, Th29, Th31;
hence mid (f,i2,i1) is_a_part<_of f,i2,i1 by FINSEQ_6:196; :: thesis: verum