let f be non constant standard special_circular_sequence; :: thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds
Int (right_cell f,k) c= RightComp f
let k be Element of NAT ; :: thesis: ( 1 <= k & k + 1 <= len f implies Int (right_cell f,k) c= RightComp f )
assume A1: ( 1 <= k & k + 1 <= len f ) ; :: thesis: Int (right_cell f,k) c= RightComp f
A2: len f = len (Rev f) by FINSEQ_5:def 3;
k <= len f by A1, NAT_1:13;
then A3: ((len f) -' k) + k = len f by XREAL_1:237;
then A4: ( 1 <= (len f) -' k & ((len f) -' k) + 1 <= len f ) by A1, XREAL_1:8;
then A5: right_cell f,k = left_cell (Rev f),((len f) -' k) by A1, A3, Th13;
RightComp f = LeftComp (Rev f) by Th26;
hence Int (right_cell f,k) c= RightComp f by A2, A4, A5, Th24; :: thesis: verum