theorem Th27: :: FINSEQ_5:27

for i, n being Nat
for D being non empty set
for f being FinSequence of D holds
( ( for f being FinSequence st i in dom (f /^ n) holds
(f /^ n) . i = f . (n + i) ) & ( i in dom (f /^ n) implies (f /^ n) /. i = f /. (n + i) ) )