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;

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

end;

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