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 A1: 1 <= len s ; :: thesis: Op-Shift (s,0) = s
then A2: ( 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 Def3;

A3: 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 A4: i in Seg (len s) by A2, FINSEQ_1:def 3;
then A5: ( 1 <= i & i <= len s ) by FINSEQ_1:1;
then A6: 1 - 1 <= i - 1 by XREAL_1:9;
i < (len s) + 1 by A5, NAT_1:13;
then A7: 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 A4, Def3, A1
.= s . ((i - 1) + 1) by A7, A6, NAT_D:63
.= s . i ; :: thesis: verum

end;

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