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)

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 )
;

end;

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;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