let i, n be Nat; :: thesis: for D being set
for f being FinSequence of D st i in dom (f /^ n) holds
(f /^ n) /. i = f /. (n + i)
let D be set ; :: thesis: for f being FinSequence of D st i in dom (f /^ n) holds
(f /^ n) /. i = f /. (n + i)
let f be FinSequence of D; :: 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)

per cases ( n <= len f or n > len f ) ;

suppose A2: n <= len f ; :: thesis: (f /^ n) /. i = f /. (n + i)

A3: n + i in dom f by A1, Th29;
thus (f /^ n) /. i = (f /^ n) . i by A1, PARTFUN1:def 8
.= f . (n + i) by A1, A2, RFINSEQ:def 2
.= f /. (n + i) by A3, PARTFUN1:def 8 ; :: thesis: verum

end;

suppose n > len f ; :: thesis: (f /^ n) /. i = f /. (n + i)

then f /^ n = <*> D by RFINSEQ:def 2;
hence (f /^ n) /. i = f /. (n + i) by A1; :: thesis: verum

end;

end;