let k be Element of NAT ; for seq being Complex_Sequence st 0 < k holds
(Shift seq) . k = seq . (k -' 1)
let seq be Complex_Sequence; ( 0 < k implies (Shift seq) . k = seq . (k -' 1) )
assume A1:
0 < k
; (Shift seq) . k = seq . (k -' 1)
then A2:
0 + 1 <= k
by INT_1:20;
consider m being Nat such that
A3:
m + 1 = k
by A1, NAT_1:6;
A4:
m = k - 1
by A3;
m in NAT
by ORDINAL1:def 13;
hence (Shift seq) . k =
seq . m
by A3, Def12
.=
seq . (k -' 1)
by A2, A4, XREAL_1:235
;
verum