let f be non constant standard special_circular_sequence; RightComp f = LeftComp (Rev f)
LeftComp (Rev f) is_a_component_of (L~ (Rev f)) `
by Def1;
then A1:
LeftComp (Rev f) is_a_component_of (L~ f) `
by SPPOL_2:22;
A2:
len f >= 4
by GOBOARD7:36;
A3:
len f >= 1 + 1
by GOBOARD7:36, XXREAL_0:2;
A4:
((len f) -' 1) + 1 = len f
by A2, XREAL_1:237, XXREAL_0:2;
then A5:
1 <= (len f) -' 1
by A3, XREAL_1:8;
A6:
((len f) -' 1) + 1 <= len (Rev f)
by A4, FINSEQ_5:def 3;
right_cell f,1 = left_cell (Rev f),((len f) -' 1)
by A4, A5, Th13;
then
Int (right_cell f,1) c= LeftComp (Rev f)
by A5, A6, Th24;
hence
RightComp f = LeftComp (Rev f)
by A1, Def2; verum