let i, n be Nat; :: thesis: for D being set
for f being FinSequence of D st i in dom (f /^ n) holds
n + i in dom f
let D be set ; :: thesis: for f being FinSequence of D st i in dom (f /^ n) holds
n + i in dom f
let f be FinSequence of D; :: thesis: ( i in dom (f /^ n) implies n + i in dom f )
assume A1: i in dom (f /^ n) ; :: thesis: n + i in dom f

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

suppose A2: n <= len f ; :: thesis: n + i in dom f

i <= len (f /^ n) by A1, FINSEQ_3:27;
then i <= (len f) - n by A2, RFINSEQ:def 2;
then A3: n + i <= len f by XREAL_1:21;
( 1 <= i & i <= i + n ) by A1, FINSEQ_3:27, NAT_1:11;
then 1 <= i + n by XXREAL_0:2;
hence n + i in dom f by A3, FINSEQ_3:27; :: thesis: verum

end;

suppose n > len f ; :: thesis: n + i in dom f

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

end;

end;