let f be non constant standard special_circular_sequence; :: thesis: for i1, i2 being Element of 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 Element of 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 Th30
.= (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) by Th30 ;
hence (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part<_of f,i1,i2 by A1, A2, A3, Th41, Th45; :: thesis: verum