let D be non empty set ; :: thesis: for p being Element of D

for f being FinSequence of D holds len (Rotate (f,p)) = len f

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

let f be FinSequence of D; :: thesis: len (Rotate (f,p)) = len f

for f being FinSequence of D holds len (Rotate (f,p)) = len f

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

let f be FinSequence of D; :: thesis: len (Rotate (f,p)) = len f

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

end;

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

then
f -: p <> {}
by FINSEQ_5:47;

then A2: 1 <= len (f -: p) by NAT_1:14;

thus len (Rotate (f,p)) = len ((f :- p) ^ ((f -: p) /^ 1)) by A1, Def2

.= (len (f :- p)) + (len ((f -: p) /^ 1)) by FINSEQ_1:22

.= (len (f :- p)) + ((len (f -: p)) - 1) by A2, RFINSEQ:def 1

.= ((len (f :- p)) + (len (f -: p))) - 1

.= ((((len f) - (p .. f)) + 1) + (len (f -: p))) - 1 by A1, FINSEQ_5:50

.= ((len f) - (p .. f)) + (len (f -: p))

.= ((len f) - (p .. f)) + (p .. f) by A1, FINSEQ_5:42

.= len f ; :: thesis: verum

end;then A2: 1 <= len (f -: p) by NAT_1:14;

thus len (Rotate (f,p)) = len ((f :- p) ^ ((f -: p) /^ 1)) by A1, Def2

.= (len (f :- p)) + (len ((f -: p) /^ 1)) by FINSEQ_1:22

.= (len (f :- p)) + ((len (f -: p)) - 1) by A2, RFINSEQ:def 1

.= ((len (f :- p)) + (len (f -: p))) - 1

.= ((((len f) - (p .. f)) + 1) + (len (f -: p))) - 1 by A1, FINSEQ_5:50

.= ((len f) - (p .. f)) + (len (f -: p))

.= ((len f) - (p .. f)) + (p .. f) by A1, FINSEQ_5:42

.= len f ; :: thesis: verum