let D be non empty set ; :: thesis: for s being FinSequence of D st 1 <= len s holds
Op-Shift (s,1) = Op-LeftShift s
let s be FinSequence of D; :: thesis: ( 1 <= len s implies Op-Shift (s,1) = Op-LeftShift s )
assume A1: 1 <= len s ; :: thesis: Op-Shift (s,1) = Op-LeftShift s
A2: ( len (Op-Shift (s,1)) = len s & ( for i being Nat st i in Seg (len s) holds
(Op-Shift (s,1)) . i = s . ((((i - 1) + 1) mod (len s)) + 1) ) ) by Def3, A1;
A3: ( Op-LeftShift s is FinSequence of D & len (Op-LeftShift s) = len s ) by A1, Th5;
A4: len <*(s . 1)*> = 1 by FINSEQ_1:40;
A5: len (s /^ 1) = (len s) - 1 by A1, RFINSEQ:def 1;

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

let i be Nat; :: thesis: ( i in dom (Op-Shift (s,1)) implies (Op-Shift (s,1)) . i = (Op-LeftShift s) . i )
assume i in dom (Op-Shift (s,1)) ; :: thesis: (Op-Shift (s,1)) . i = (Op-LeftShift s) . i
then A6: i in Seg (len s) by A2, FINSEQ_1:def 3;
then A7: ( 1 <= i & i <= len s ) by FINSEQ_1:1;

now :: thesis: (Op-Shift (s,1)) . i = (Op-LeftShift s) . i

per cases ( i = len s or i <> len s ) ;

suppose A8: i = len s ; :: thesis: (Op-Shift (s,1)) . i = (Op-LeftShift s) . i

A9: (Op-Shift (s,1)) . i = s . ((((i - 1) + 1) mod (len s)) + 1) by A6, Def3, A1
.= s . (0 + 1) by A1, A8, INT_1:62
.= s . 1 ;
A10: i <= (len (s /^ 1)) + (len <*(s . 1)*>) by A8, A5, A4;
A11: i - (len (s /^ 1)) = (len s) - ((len s) - 1) by A8, A1, RFINSEQ:def 1;
(Op-LeftShift s) . i = <*(s . 1)*> . 1 by A10, A4, A11, FINSEQ_1:23
.= s . 1 ;
hence (Op-Shift (s,1)) . i = (Op-LeftShift s) . i by A9; :: thesis: verum

end;

suppose i <> len s ; :: thesis: (Op-Shift (s,1)) . i = (Op-LeftShift s) . i

then A12: ( 0 <= i & i < len s ) by A7, XXREAL_0:1;
i + 1 <= len s by A12, NAT_1:13;
then A13: (i + 1) - 1 <= (len s) - 1 by XREAL_1:9;
then A14: ( 1 <= i & i <= (len s) - 1 ) by A6, FINSEQ_1:1;
reconsider ls1 = (len s) - 1 as Element of NAT by A13, INT_1:3;
i in Seg ls1 by A14;
then A15: i in dom (s /^ 1) by A5, FINSEQ_1:def 3;
A16: (Op-Shift (s,1)) . i = s . ((((i - 1) + 1) mod (len s)) + 1) by A6, Def3, A1
.= s . (i + 1) by A12, NAT_D:63 ;
(Op-LeftShift s) . i = (s /^ 1) . i by A5, A14, FINSEQ_1:64
.= s . (i + 1) by A15, A1, RFINSEQ:def 1 ;
hence (Op-Shift (s,1)) . i = (Op-LeftShift s) . i by A16; :: thesis: verum

end;

end;

end;

hence (Op-Shift (s,1)) . i = (Op-LeftShift s) . i ; :: thesis: verum

end;

hence Op-Shift (s,1) = Op-LeftShift s by A2, A3, FINSEQ_2:9; :: thesis: verum