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, Th98;
then A3: (Rotate f9,p) :- p = Rotate f,p by Th48;
A4: p in rng (Rotate f,p) by A1, Th97;
A5: len <*p*> = 1 by FINSEQ_1:56;
(Rotate f9,p) -: p = <*p*> by A2, Th48;
hence Rotate (Rotate f,p),p = (Rotate f,p) ^ (<*p*> /^ 1) by A3, A4, Def2
.= (Rotate f,p) ^ {} by A5, 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;