let D be non empty set ; :: thesis: for f being FinSequence of D holds Rotate (f,(f /. 1)) = f
let f be FinSequence of D; :: thesis: Rotate (f,(f /. 1)) = f
A1: len <*(f /. 1)*> = 1 by FINSEQ_1:39;

per cases ( not f is empty or f is empty ) ;

suppose A2: not f is empty ; :: thesis: Rotate (f,(f /. 1)) = f

then f /. 1 in rng f by Th42;
hence Rotate (f,(f /. 1)) = (f :- (f /. 1)) ^ ((f -: (f /. 1)) /^ 1) by Def2
.= f ^ ((f -: (f /. 1)) /^ 1) by A2, Th44
.= f ^ (<*(f /. 1)*> /^ 1) by A2, Th44
.= f ^ {} by A1, FINSEQ_5:32
.= f by FINSEQ_1:34 ;
:: thesis: verum

end;

suppose f is empty ; :: thesis: Rotate (f,(f /. 1)) = f

hence Rotate (f,(f /. 1)) = f by Def2, RELAT_1:38; :: thesis: verum

end;

end;