let f be non constant standard special_circular_sequence; :: thesis: LeftComp f <> RightComp f
set g = Rotate f,(N-min (L~ f));
A1: L~ f = L~ (Rotate f,(N-min (L~ f))) by REVROT_1:33;
N-min (L~ f) in rng f by SPRECT_2:43;
then A2: (Rotate f,(N-min (L~ f))) /. 1 = N-min (L~ (Rotate f,(N-min (L~ f)))) by A1, FINSEQ_6:98;
A3: RightComp (Rotate f,(N-min (L~ f))) = RightComp f by REVROT_1:37;
LeftComp (Rotate f,(N-min (L~ f))) = LeftComp f by REVROT_1:36;
hence LeftComp f <> RightComp f by A2, A3, Lm2; :: thesis: verum