let k, i be Element of NAT ; :: thesis: for p being FinSequence st k in dom p holds
(Seq (i Shift p)) . k = p . k
let p be FinSequence; :: thesis: ( k in dom p implies (Seq (i Shift p)) . k = p . k )
assume A1: k in dom p ; :: thesis: (Seq (i Shift p)) . k = p . k
then A2: k in dom (Seq (i Shift p)) by Th58;
A3: Seq (i Shift p) = (i Shift p) * (Sgm (dom (i Shift p))) by FINSEQ_1:def 14;
A4: (Seq (i Shift p)) . k = ((i Shift p) * (Sgm (dom (i Shift p)))) . k by FINSEQ_1:def 14;
((i Shift p) * (Sgm (dom (i Shift p)))) . k = (i Shift p) . ((Sgm (dom (i Shift p))) . k) by A2, A3, FUNCT_1:12
.= (i Shift p) . (i + k) by A1, Th59 ;
hence (Seq (i Shift p)) . k = p . k by A1, A4, Def15; :: thesis: verum