let k be Nat; :: thesis: for D being set
for f being FinSequence of D st 1 <= k holds
((k + 1),(len f)) -cut f = f /^ k
let D be set ; :: thesis: for f being FinSequence of D st 1 <= k holds
((k + 1),(len f)) -cut f = f /^ k
let f be FinSequence of D; :: thesis: ( 1 <= k implies ((k + 1),(len f)) -cut f = f /^ k )
assume A1: 1 <= k ; :: thesis: ((k + 1),(len f)) -cut f = f /^ k

per cases ( len f < k or f = {} or k <= len f ) ;

suppose A2: len f < k ; :: thesis: ((k + 1),(len f)) -cut f = f /^ k

k <= k + 1 by NAT_1:11;
then len f < k + 1 by A2, XXREAL_0:2;
hence ((k + 1),(len f)) -cut f = {} by FINSEQ_6:def 4
.= f /^ k by A2, FINSEQ_5:32 ;
:: thesis: verum

end;

suppose A3: f = {} ; :: thesis: ((k + 1),(len f)) -cut f = f /^ k

then A4: len f = 0 ;
thus ((k + 1),(len f)) -cut f = <*> D by A3, FINSEQ_6:def 4
.= f /^ k by A1, A4, RFINSEQ:def 1 ; :: thesis: verum

end;

suppose A5: k <= len f ; :: thesis: ((k + 1),(len f)) -cut f = f /^ k

set IT = ((k + 1),(len f)) -cut f;
A6: 1 <= k + 1 by NAT_1:11;
A7: k + 1 <= (len f) + 1 by A5, XREAL_1:6;
A8: for m being Nat st m in dom (((k + 1),(len f)) -cut f) holds
(((k + 1),(len f)) -cut f) . m = f . (m + k)

proof

let m be Nat; :: thesis: ( m in dom (((k + 1),(len f)) -cut f) implies (((k + 1),(len f)) -cut f) . m = f . (m + k) )
assume A9: m in dom (((k + 1),(len f)) -cut f) ; :: thesis: (((k + 1),(len f)) -cut f) . m = f . (m + k)
1 <= m by A9, FINSEQ_3:25;
then consider i being Nat such that
A10: m = 1 + i by NAT_1:10;
reconsider i = i as Nat ;
m <= len (((k + 1),(len f)) -cut f) by A9, FINSEQ_3:25;
then i < len (((k + 1),(len f)) -cut f) by A10, NAT_1:13;
hence (((k + 1),(len f)) -cut f) . m = f . ((k + 1) + i) by A6, A7, A10, Lm1
.= f . (m + k) by A10 ;
:: thesis: verum

end;

(len f) + 1 = (len (((k + 1),(len f)) -cut f)) + (k + 1) by A6, A7, Lm1
.= ((len (((k + 1),(len f)) -cut f)) + k) + 1 ;
then len (((k + 1),(len f)) -cut f) = (len f) - k ;
hence ((k + 1),(len f)) -cut f = f /^ k by A5, A8, RFINSEQ:def 1; :: thesis: verum

end;

end;