let D be non empty set ; :: thesis: for f being FinSequence of D
for i, n being Nat st i in dom (f /^ n) holds
(f /^ n) . i = f . (n + i)
let f be FinSequence of D; :: thesis: for i, n being Nat st i in dom (f /^ n) holds
(f /^ n) . i = f . (n + i)
let i, n be Nat; :: thesis: ( i in dom (f /^ n) implies (f /^ n) . i = f . (n + i) )
assume A1: i in dom (f /^ n) ; :: thesis: (f /^ n) . i = f . (n + i)
reconsider i = i, n = n as Element of NAT by ORDINAL1:def 12;
A2: n + i in dom f by A1, FINSEQ_5:26;
( (f /^ n) /. i = f /. (n + i) & (f /^ n) /. i = (f /^ n) . i ) by A1, FINSEQ_5:27, PARTFUN1:def 6;
hence (f /^ n) . i = f . (n + i) by A2, PARTFUN1:def 6; :: thesis: verum