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

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

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

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

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;

end;