per cases ( not p in rng f or ( p in rng f & p <> f /. 1 ) or ( p in rng f & p = f /. 1 ) ) ;

suppose not p in rng f ; :: thesis: Rotate (f,p) is circular

hence Rotate (f,p) is circular by Def2; :: thesis: verum

end;

suppose that A1: p in rng f and
A2: p <> f /. 1 ; :: thesis: Rotate (f,p) is circular

A3: p .. f >= 1 by A1, FINSEQ_4:21;
A4: Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by A1, Def2;
p .. f <> 1 by A1, A2, FINSEQ_5:38;
then p .. f > 1 by A3, XXREAL_0:1;
then p .. f >= 1 + 1 by NAT_1:13;
then A5: len (f -: p) >= 1 + 1 by A1, FINSEQ_5:42;
then 1 <= len (f -: p) by XXREAL_0:2;
then A6: len ((f -: p) /^ 1) = (len (f -: p)) - 1 by RFINSEQ:def 1;
then (len ((f -: p) /^ 1)) + 1 = len (f -: p) ;
then len ((f -: p) /^ 1) >= 1 by A5, XREAL_1:6;
then A7: len ((f -: p) /^ 1) in dom ((f -: p) /^ 1) by FINSEQ_3:25;
1 in dom (f :- p) by FINSEQ_5:6;
hence (Rotate (f,p)) /. 1 = (f :- p) /. 1 by A4, FINSEQ_4:68
.= p by FINSEQ_5:53
.= (f -: p) /. (p .. f) by A1, FINSEQ_5:45
.= (f -: p) /. ((len ((f -: p) /^ 1)) + 1) by A1, A6, FINSEQ_5:42
.= ((f -: p) /^ 1) /. (len ((f -: p) /^ 1)) by A7, FINSEQ_5:27
.= ((f :- p) ^ ((f -: p) /^ 1)) /. ((len (f :- p)) + (len ((f -: p) /^ 1))) by A7, FINSEQ_4:69
.= (Rotate (f,p)) /. (len (Rotate (f,p))) by A4, FINSEQ_1:22 ;
:: according to FINSEQ_6:def 1 :: thesis: verum

end;

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

hence Rotate (f,p) is circular by Th89; :: thesis: verum

end;

end;