let D be non empty set ; :: thesis: for s being FinSequence of D st 1 <= len s holds
Op-Shift (s,0) = s
let s be FinSequence of D; :: thesis: ( 1 <= len s implies Op-Shift (s,0) = s )
assume AS: 1 <= len s ; :: thesis: Op-Shift (s,0) = s
then A1: ( len (Op-Shift (s,0)) = len s & ( for i being Nat st i in Seg (len s) holds
(Op-Shift (s,0)) . i = s . ((((i - 1) + 0) mod (len s)) + 1) ) ) by defShift;

A2: now :: thesis: for i being Nat st i in dom (Op-Shift (s,0)) holds
(Op-Shift (s,0)) . i = s . i

let i be Nat; :: thesis: ( i in dom (Op-Shift (s,0)) implies (Op-Shift (s,0)) . i = s . i )
assume i in dom (Op-Shift (s,0)) ; :: thesis: (Op-Shift (s,0)) . i = s . i
then A32: i in Seg (len s) by A1, FINSEQ_1:def 3;
then P31: ( 1 <= i & i <= len s ) by FINSEQ_1:1;
then P32: 1 - 1 <= i - 1 by XREAL_1:9;
i < (len s) + 1 by P31, NAT_1:13;
then P33: i - 1 < ((len s) + 1) - 1 by XREAL_1:14;
thus (Op-Shift (s,0)) . i = s . ((((i - 1) + 0) mod (len s)) + 1) by A32, defShift, AS
.= s . ((i - 1) + 1) by P33, P32, NAT_D:63
.= s . i ; :: thesis: verum

end;

thus Op-Shift (s,0) = s by A1, A2, FINSEQ_2:9; :: thesis: verum