let n be Nat; :: thesis: for f being FinSequence of REAL
for k being positive Nat st n + k in dom f holds
k in dom (f /^ n)
let f be FinSequence of REAL ; :: thesis: for k being positive Nat st n + k in dom f holds
k in dom (f /^ n)
let k be positive Nat; :: thesis: ( n + k in dom f implies k in dom (f /^ n) )
A0: k >= 1 by NAT_1:14;
assume n + k in dom f ; :: thesis: k in dom (f /^ n)
then A2: n + k <= len f by FINSEQ_3:25;
then A3: (n + k) - n <= (len f) - n by XREAL_1:9;
n + k > n + 0 by XREAL_1:6;
then len f > n by A2, XXREAL_0:2;
then k <= len (f /^ n) by A3, RFINSEQ:def 1;
hence k in dom (f /^ n) by A0, FINSEQ_3:25; :: thesis: verum