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

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