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,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part<_of f,i1,i2
let i1, i2 be Nat; :: thesis: ( 1 <= i1 & i1 < i2 & i2 < len f implies (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part<_of f,i1,i2 )
assume that
A1: 1 <= i1 and
A2: i1 < i2 and
A3: i2 < len f ; :: thesis: (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part<_of f,i1,i2
Rev ((mid (f,i2,((len f) -' 1))) ^ (mid (f,1,i1))) = (Rev (mid (f,1,i1))) ^ (Rev (mid (f,i2,((len f) -' 1)))) by FINSEQ_5:64
.= (mid (f,i1,1)) ^ (Rev (mid (f,i2,((len f) -' 1)))) by FINSEQ_6:196
.= (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) by FINSEQ_6:196 ;
hence (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part<_of f,i1,i2 by A1, A2, A3, Th29, Th33; :: thesis: verum