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

per cases ( 0 + 1 > k or 1 <= k ) ;

suppose A2: 0 + 1 > k ; :: thesis: (1,k) -cut f = f | k

A3: f | 0 = {} ;
k = 0 by A2, NAT_1:13;
hence (1,k) -cut f = f | k by A3, FINSEQ_6:def 4; :: thesis: verum

end;

suppose A4: 1 <= k ; :: thesis: (1,k) -cut f = f | k

A5: (len (f | k)) + 1 = k + 1 by A1, FINSEQ_1:59;
for i being Nat st i < len (f | k) holds
(f | k) . (i + 1) = f . (1 + i)

proof

let i be Nat; :: thesis: ( i < len (f | k) implies (f | k) . (i + 1) = f . (1 + i) )
assume i < len (f | k) ; :: thesis: (f | k) . (i + 1) = f . (1 + i)
then i + 1 <= k by A5, NAT_1:13;
hence (f | k) . (i + 1) = f . (1 + i) by FINSEQ_3:112; :: thesis: verum

end;

hence (1,k) -cut f = f | k by A1, A4, A5, FINSEQ_6:def 4; :: thesis: verum

end;

end;