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

proof

let f be FinSequence; :: 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 n <= len f ; :: thesis: (f /^ n) . i = f . (n + i)

hence (f /^ n) . i = f . (n + i) by A1, RFINSEQ:def 1; :: thesis: verum

end;

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

then f /^ n = {} by RFINSEQ:def 1;
hence (f /^ n) . i = f . (n + i) by A1; :: thesis: verum

end;

end;

end;

assume B1: i in dom (f /^ n) ; :: thesis: (f /^ n) /. i = f /. (n + i)
then B2: n + i in dom f by Th26;
(f /^ n) . i = f . (n + i) by AA, B1;
then (f /^ n) /. i = f . (n + i) by B1, PARTFUN1:def 6
.= f /. (n + i) by PARTFUN1:def 6, B2 ;
hence (f /^ n) /. i = f /. (n + i) ; :: thesis: verum