let n, k be Nat; :: thesis: ( k in Seg (n + 1) implies ex l, m being Nat st
( l = k - 1 & m = n - l ) )
assume A1: k in Seg (n + 1) ; :: thesis: ex l, m being Nat st
( l = k - 1 & m = n - l )
reconsider k = k as non zero Nat by A1, FINSEQ_1:1;
reconsider l = k - 1 as Nat ;
(n - (k - 1)) + k >= 0 + k by A1, FINSEQ_1:1;
then n - l >= 0 by XREAL_1:6;
hence ex l, m being Nat st
( l = k - 1 & m = n - l ) ; :: thesis: verum