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
LeftComp (Rotate f,p) is_a_component_of (L~ (Rotate f,p)) ` by GOBOARD9:def 1;
then A1: LeftComp (Rotate f,p) is_a_component_of (L~ f) ` by Th33;
A2: ( p in rng f implies p .. f >= 1 ) by FINSEQ_4:31;

per cases ( not p in rng f or ( p in rng f & p .. f = 1 ) or ( p in rng f & 1 < p .. f ) ) by A2, 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 that A3: p in rng f and
A4: p .. f = 1 ; :: thesis: LeftComp (Rotate f,p) = LeftComp f

A5: 1 in dom f by FINSEQ_5:6;
f . 1 = p by A3, A4, FINSEQ_4:29;
then f /. 1 = p by A5, PARTFUN1:def 8;
hence LeftComp (Rotate f,p) = LeftComp f by FINSEQ_6:95; :: thesis: verum

end;

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

A8: p .. f <= len f by A6, FINSEQ_4:31;
then A9: 1 + (p .. f) <= 1 + (len f) by XREAL_1:8;
A10: len f <= (len f) + 1 by NAT_1:11;
1 + 1 <= p .. f by A7, NAT_1:13;
then (1 + 1) + (len f) <= (len f) + (p .. f) by XREAL_1:8;
then ((1 + (len f)) + 1) -' (p .. f) <= len f by NAT_D:53;
then ((1 + (len f)) -' (p .. f)) + 1 <= len f by A8, A10, NAT_D:38, XXREAL_0:2;
then A11: ((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 A6, A7, Th35;
then Int (left_cell f,1) c= LeftComp (Rotate f,p) by A9, A11, GOBOARD9:24, NAT_D:55;
hence LeftComp (Rotate f,p) = LeftComp f by A1, GOBOARD9:def 1; :: thesis: verum

end;

end;