let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D holds Rotate ((Rotate (f,p)),p) = Rotate (f,p)
let p be Element of D; :: thesis: for f being FinSequence of D holds Rotate ((Rotate (f,p)),p) = Rotate (f,p)
let f be FinSequence of D; :: thesis: Rotate ((Rotate (f,p)),p) = Rotate (f,p)

per cases ( p in rng f or not p in rng f ) ;

suppose A1: p in rng f ; :: thesis: Rotate ((Rotate (f,p)),p) = Rotate (f,p)

then reconsider f9 = f as non empty FinSequence of D ;
A2: (Rotate (f,p)) /. 1 = p by A1, Th92;
then A3: (Rotate (f9,p)) :- p = Rotate (f,p) by Th44;
A4: p in rng (Rotate (f,p)) by A1, Th91;
A5: len <*p*> = 1 by FINSEQ_1:39;
(Rotate (f9,p)) -: p = <*p*> by A2, Th44;
hence Rotate ((Rotate (f,p)),p) = (Rotate (f,p)) ^ (<*p*> /^ 1) by A3, A4, Def2
.= (Rotate (f,p)) ^ {} by A5, FINSEQ_5:32
.= Rotate (f,p) by FINSEQ_1:34 ;
:: thesis: verum

end;

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

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

end;

end;