let p be Point of (TOP-REAL 2); :: thesis: for f being V8() standard special_circular_sequence holds LeftComp (Rotate f,p) = LeftComp f
let f be V8() standard special_circular_sequence; :: thesis: LeftComp (Rotate f,p) = LeftComp f
A1: ( p in rng f implies p .. f >= 1 ) by FINSEQ_4:31;
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:29, FINSEQ_5:6;
then f /. 1 = p by PARTFUN1:def 8;
hence LeftComp (Rotate f,p) = LeftComp f by FINSEQ_6:95; :: 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:31;
then A6: 1 + (p .. f) <= 1 + (len f) by XREAL_1:8;
1 + 1 <= p .. f by A4, NAT_1:13;
then (1 + 1) + (len f) <= (len f) + (p .. f) by XREAL_1:8;
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:24, NAT_D:55;
hence LeftComp (Rotate f,p) = LeftComp f by A2, GOBOARD9:def 1; :: thesis: verum

end;

end;