let k be Element of 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 GRAPH_2:def 1
.= f /^ k by A2, FINSEQ_5:35 ;
:: thesis: verum

end;

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

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

end;

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

A5: 1 <= k + 1 by NAT_1:11;
set IT = (k + 1),(len f) -cut f;
A6: k + 1 <= (len f) + 1 by A4, XREAL_1:8;
then (len f) + 1 = (len ((k + 1),(len f) -cut f)) + (k + 1) by A5, Lm1
.= ((len ((k + 1),(len f) -cut f)) + k) + 1 ;
then A7: len ((k + 1),(len f) -cut f) = (len f) - k ;
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 A8: m in dom ((k + 1),(len f) -cut f) ; :: thesis: ((k + 1),(len f) -cut f) . m = f . (m + k)
1 <= m by A8, FINSEQ_3:27;
then consider i being Nat such that
A9: m = 1 + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
m <= len ((k + 1),(len f) -cut f) by A8, FINSEQ_3:27;
then i < len ((k + 1),(len f) -cut f) by A9, NAT_1:13;
hence ((k + 1),(len f) -cut f) . m = f . ((k + 1) + i) by A5, A6, A9, Lm1
.= f . (m + k) by A9 ;
:: thesis: verum

end;

hence (k + 1),(len f) -cut f = f /^ k by A4, A7, RFINSEQ:def 2; :: thesis: verum

end;

end;