let f be non constant standard special_circular_sequence; :: thesis: 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; :: thesis: verum

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; :: thesis: verum