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:67
.= (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