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 ;
A4: Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by ;
p .. f <> 1 by ;
then p .. f > 1 by ;
then p .. f >= 1 + 1 by NAT_1:13;
then A5: len (f -: p) >= 1 + 1 by ;
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 ;
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
.= p by FINSEQ_5:53
.= (f -: p) /. (p .. f) by
.= (f -: p) /. ((len ((f -: p) /^ 1)) + 1) by
.= ((f -: p) /^ 1) /. (len ((f -: p) /^ 1)) by
.= ((f :- p) ^ ((f -: p) /^ 1)) /. ((len (f :- p)) + (len ((f -: p) /^ 1))) by
.= (Rotate (f,p)) /. (len (Rotate (f,p))) by ;
:: 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;