let p be Point of (TOP-REAL 2); :: thesis: for f being constant standard special_circular_sequence holds LeftComp (Rotate (f,p)) = LeftComp f
let f be constant standard special_circular_sequence; :: thesis: LeftComp (Rotate (f,p)) = LeftComp f
A1: ( p in rng f implies p .. f >= 1 ) by FINSEQ_4:21;
LeftComp (Rotate (f,p)) is_a_component_of (L~ (Rotate (f,p))) ` by GOBOARD9:def 1;
then A2: LeftComp (Rotate (f,p)) is_a_component_of (L~ f) ` by Th33;

per cases ( not p in rng f or ( p in rng f & p .. f = 1 ) or ( p in rng f & 1 < p .. f ) ) by A1, XXREAL_0:1;

suppose not p in rng f ; :: thesis: LeftComp (Rotate (f,p)) = LeftComp f

hence LeftComp (Rotate (f,p)) = LeftComp f by FINSEQ_6:def 2; :: thesis: verum

end;

suppose ( p in rng f & p .. f = 1 ) ; :: thesis: LeftComp (Rotate (f,p)) = LeftComp f

then ( 1 in dom f & f . 1 = p ) by FINSEQ_4:19, FINSEQ_5:6;
then f /. 1 = p by PARTFUN1:def 6;
hence LeftComp (Rotate (f,p)) = LeftComp f by FINSEQ_6:89; :: thesis: verum

end;

suppose that A3: p in rng f and
A4: 1 < p .. f ; :: thesis: LeftComp (Rotate (f,p)) = LeftComp f

A5: p .. f <= len f by A3, FINSEQ_4:21;
then A6: 1 + (p .. f) <= 1 + (len f) by XREAL_1:6;
1 + 1 <= p .. f by A4, NAT_1:13;
then (1 + 1) + (len f) <= (len f) + (p .. f) by XREAL_1:6;
then ( len f <= (len f) + 1 & ((1 + (len f)) + 1) -' (p .. f) <= len f ) by NAT_1:11, NAT_D:53;
then ((1 + (len f)) -' (p .. f)) + 1 <= len f by A5, NAT_D:38, XXREAL_0:2;
then A7: ((1 + (len f)) -' (p .. f)) + 1 <= len (Rotate (f,p)) by Th14;
left_cell (f,1) = left_cell ((Rotate (f,p)),((1 + (len f)) -' (p .. f))) by A3, A4, Th35;
then Int (left_cell (f,1)) c= LeftComp (Rotate (f,p)) by A6, A7, GOBOARD9:21, NAT_D:55;
hence LeftComp (Rotate (f,p)) = LeftComp f by A2, GOBOARD9:def 1; :: thesis: verum

end;

end;