let n be Nat; :: thesis: for f being FinSequence
for i being non zero Nat holds f . (n + i) = (f /^ n) . i
let f be FinSequence; :: thesis: for i being non zero Nat holds f . (n + i) = (f /^ n) . i
let i be non zero Nat; :: thesis: f . (n + i) = (f /^ n) . i
consider D being non empty set such that
A0: f is FinSequence of D by Th0;
reconsider f = f as FinSequence of D by A0;

per cases ( not i in dom (f /^ n) or i in dom (f /^ n) ) ;

suppose B1: not i in dom (f /^ n) ; :: thesis: f . (n + i) = (f /^ n) . i

B2: (f /^ n) . i = 0 by B1, FUNCT_1:def 2;
n + i > len f

proof

i >= 1 by NAT_1:14;
then i > len (f /^ n) by B1, FINSEQ_3:25;
then C1: i > (len f) -' n by RFINSEQ:29;

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

suppose D1: len f < n ; :: thesis: n + i > len f

n + i >= n + 0 by XREAL_1:6;
hence n + i > len f by D1, XXREAL_0:2; :: thesis: verum

end;

suppose len f >= n ; :: thesis: n + i > len f

then (len f) - n >= n - n by XREAL_1:9;
then (len f) -' n = (len f) - n by XREAL_0:def 2;
then i + n > ((len f) - n) + n by C1, XREAL_1:6;
hence n + i > len f ; :: thesis: verum

end;

end;

end;

then not n + i in dom f by FINSEQ_3:25;
hence f . (n + i) = (f /^ n) . i by B2, FUNCT_1:def 2; :: thesis: verum

end;

suppose i in dom (f /^ n) ; :: thesis: f . (n + i) = (f /^ n) . i

hence f . (n + i) = (f /^ n) . i by FINSEQ_7:4; :: thesis: verum

end;

end;