let D be non empty set ; :: thesis: for f being circular FinSequence of D
for p being Element of D st ( for i being Nat st 1 < i & i < len f holds
f /. i <> f /. 1 ) holds
Rotate ((Rotate (f,p)),(f /. 1)) = f

let f be circular FinSequence of D; :: thesis: for p being Element of D st ( for i being Nat st 1 < i & i < len f holds
f /. i <> f /. 1 ) holds
Rotate ((Rotate (f,p)),(f /. 1)) = f

let p be Element of D; :: thesis: ( ( for i being Nat st 1 < i & i < len f holds
f /. i <> f /. 1 ) implies Rotate ((Rotate (f,p)),(f /. 1)) = f )

assume A1: for i being Nat st 1 < i & i < len f holds
f /. i <> f /. 1 ; :: thesis: Rotate ((Rotate (f,p)),(f /. 1)) = f
per cases ( not p in rng f or p = f /. 1 or ( p in rng f & p <> f /. 1 ) ) ;
suppose not p in rng f ; :: thesis: Rotate ((Rotate (f,p)),(f /. 1)) = f
hence Rotate ((Rotate (f,p)),(f /. 1)) = Rotate (f,(f /. 1)) by Def2
.= f by Th89 ;
:: thesis: verum
end;
suppose p = f /. 1 ; :: thesis: Rotate ((Rotate (f,p)),(f /. 1)) = f
hence Rotate ((Rotate (f,p)),(f /. 1)) = Rotate (f,(f /. 1)) by Th93
.= f by Th89 ;
:: thesis: verum
end;
suppose that A2: p in rng f and
A3: p <> f /. 1 ; :: thesis: Rotate ((Rotate (f,p)),(f /. 1)) = f
A4: f /. 1 = (f -: p) /. 1 by ;
A5: f /. 1 = f /. (len f) by Def1A;
then A6: f /. 1 = (f :- p) /. (len (f :- p)) by ;
then A7: f /. 1 in rng (f :- p) by Th3;
A8: f :- p just_once_values f /. 1
proof
( p .. f <> 1 & p .. f >= 1 ) by ;
then A9: p .. f > 1 by XXREAL_0:1;
take len (f :- p) ; :: according to FINSEQ_6:def 12 :: thesis: ( len (f :- p) in dom (f :- p) & f /. 1 = (f :- p) /. (len (f :- p)) & ( for z being set st z in dom (f :- p) & z <> len (f :- p) holds
(f :- p) /. z <> f /. 1 ) )

thus len (f :- p) in dom (f :- p) by FINSEQ_5:6; :: thesis: ( f /. 1 = (f :- p) /. (len (f :- p)) & ( for z being set st z in dom (f :- p) & z <> len (f :- p) holds
(f :- p) /. z <> f /. 1 ) )

thus f /. 1 = (f :- p) /. (len (f :- p)) by ; :: thesis: for z being set st z in dom (f :- p) & z <> len (f :- p) holds
(f :- p) /. z <> f /. 1

let z be set ; :: thesis: ( z in dom (f :- p) & z <> len (f :- p) implies (f :- p) /. z <> f /. 1 )
assume A10: z in dom (f :- p) ; :: thesis: ( not z <> len (f :- p) or (f :- p) /. z <> f /. 1 )
then reconsider k = z as Element of NAT ;
k <> 0 by ;
then consider i being Nat such that
A11: k = i + 1 by NAT_1:6;
assume A12: z <> len (f :- p) ; :: thesis: (f :- p) /. z <> f /. 1
reconsider i = i as Element of NAT by ORDINAL1:def 12;
k <= len (f :- p) by ;
then k < len (f :- p) by ;
then i + 1 < ((len f) - (p .. f)) + 1 by ;
then i < (len f) - (p .. f) by XREAL_1:6;
then A13: i + (p .. f) < len f by XREAL_1:20;
p .. f <= i + (p .. f) by NAT_1:11;
then A14: 1 < i + (p .. f) by ;
(f :- p) /. (i + 1) = f /. (i + (p .. f)) by ;
hence (f :- p) /. z <> f /. 1 by A1, A11, A14, A13; :: thesis: verum
end;
f /. 1 in rng f by ;
then A15: f /. 1 in rng (Rotate (f,p)) by ;
Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by ;
hence Rotate ((Rotate (f,p)),(f /. 1)) = (((f :- p) ^ ((f -: p) /^ 1)) :- (f /. 1)) ^ ((((f :- p) ^ ((f -: p) /^ 1)) -: (f /. 1)) /^ 1) by
.= (((f :- p) :- (f /. 1)) ^ ((f -: p) /^ 1)) ^ ((((f :- p) ^ ((f -: p) /^ 1)) -: (f /. 1)) /^ 1) by
.= (((f :- p) :- (f /. 1)) ^ ((f -: p) /^ 1)) ^ (((f :- p) -: (f /. 1)) /^ 1) by
.= (<*(f /. 1)*> ^ ((f -: p) /^ 1)) ^ (((f :- p) -: (f /. 1)) /^ 1) by A6, A8, Th5
.= (f -: p) ^ (((f :- p) -: (f /. 1)) /^ 1) by
.= (f -: p) ^ ((f :- p) /^ 1) by A6, A8, Th4
.= f by ;
:: thesis: verum
end;
end;