let k be Nat; for X being non empty ZeroStr
for seq being sequence of X st 0 < k holds
(Shift seq) . k = seq . (k -' 1)
let X be non empty ZeroStr ; for seq being sequence of X st 0 < k holds
(Shift seq) . k = seq . (k -' 1)
let seq be sequence of X; ( 0 < k implies (Shift seq) . k = seq . (k -' 1) )
A1:
k in NAT
by ORDINAL1:def 12;
assume A2:
0 < k
; (Shift seq) . k = seq . (k -' 1)
then A3:
0 + 1 <= k
by INT_1:7, A1;
consider m being Nat such that
A4:
m + 1 = k
by A2, NAT_1:6;
A5:
m = k - 1
by A4;
thus (Shift seq) . k =
seq . m
by A4, Def5
.=
seq . (k -' 1)
by A3, A5, XREAL_1:233
; verum