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 13;
A2: (f /^ n) /. i = f /. (n + i) by A1, FINSEQ_5:30;
A3: (f /^ n) /. i = (f /^ n) . i by A1, PARTFUN1:def 8;
n + i in dom f by A1, FINSEQ_5:29;
hence (f /^ n) . i = f . (n + i) by A2, A3, PARTFUN1:def 8; :: thesis: verum