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:34;
A3:
len f >= 1 + 1
by GOBOARD7:34, XXREAL_0:2;
A4:
((len f) -' 1) + 1 = len f
by A2, XREAL_1:235, XXREAL_0:2;
then A5:
1 <= (len f) -' 1
by A3, XREAL_1:6;
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, Th9;
then
Int (right_cell (f,1)) c= LeftComp (Rev f)
by A5, A6, Th19;
hence
RightComp f = LeftComp (Rev f)
by A1, Def2; verum