let i, n be Nat; :: thesis: for f being FinSequence st i in dom (f /^ n) holds
n + i in dom f
let f be FinSequence; :: 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:25;
then i <= (len f) - n by A2, RFINSEQ:def 1;
then A3: n + i <= len f by XREAL_1:19;
( 1 <= i & i <= i + n ) by A1, FINSEQ_3:25, NAT_1:11;
then 1 <= i + n by XXREAL_0:2;
hence n + i in dom f by A3, FINSEQ_3:25; :: thesis: verum

end;

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

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

end;

end;