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:31;
A4: Rotate f,p = (f :- p) ^ ((f -: p) /^ 1) by A1, Def2;
p .. f <> 1 by A1, A2, FINSEQ_5:41;
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:45;
then 1 <= len (f -: p) by XXREAL_0:2;
then A6: len ((f -: p) /^ 1) = (len (f -: p)) - 1 by RFINSEQ:def 2;
then (len ((f -: p) /^ 1)) + 1 = len (f -: p) ;
then len ((f -: p) /^ 1) >= 1 by A5, XREAL_1:8;
then A7: len ((f -: p) /^ 1) in dom ((f -: p) /^ 1) by FINSEQ_3:27;
1 in dom (f :- p) by FINSEQ_5:6;
hence (Rotate f,p) /. 1 = (f :- p) /. 1 by A4, FINSEQ_4:83
.= p by FINSEQ_5:56
.= (f -: p) /. (p .. f) by A1, FINSEQ_5:48
.= (f -: p) /. ((len ((f -: p) /^ 1)) + 1) by A1, A6, FINSEQ_5:45
.= ((f -: p) /^ 1) /. (len ((f -: p) /^ 1)) by A7, FINSEQ_5:30
.= ((f :- p) ^ ((f -: p) /^ 1)) /. ((len (f :- p)) + (len ((f -: p) /^ 1))) by A7, FINSEQ_4:84
.= (Rotate f,p) /. (len (Rotate f,p)) by A4, FINSEQ_1:35 ;
:: 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 Th95; :: thesis: verum

end;

end;