let k be 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)
A2:
0 + 1 <= k
by INT_1:7, A1;
consider m being Nat such that
A3:
m + 1 = k
by A1, NAT_1:6;
A4:
m = k - 1
by A3;
thus (Shift seq) . k =
seq . m
by A3, Def8
.=
seq . (k -' 1)
by A2, A4, XREAL_1:233
; verum