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 f' = f as non empty FinSequence of D ;
(Rotate f,p) /. 1 = p by A1, Th98;
then A2: ( (Rotate f',p) -: p = <*p*> & (Rotate f',p) :- p = Rotate f,p ) by Th48;
A3: len <*p*> = 1 by FINSEQ_1:56;
p in rng (Rotate f,p) by A1, Th97;
hence Rotate (Rotate f,p),p = (Rotate f,p) ^ (<*p*> /^ 1) by A2, Def2
.= (Rotate f,p) ^ {} by A3, FINSEQ_5:35
.= Rotate f,p by FINSEQ_1:47 ;
:: 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;