let n, i be Nat; :: thesis: ( i in Seg n implies ex j, k being Nat st
( n = (j + 1) + k & i = j + 1 ) )
assume A1: i in Seg n ; :: thesis: ex j, k being Nat st
( n = (j + 1) + k & i = j + 1 )
then 1 <= i by FINSEQ_1:1;
then consider j being Nat such that
A2: i = 1 + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
i <= n by A1, FINSEQ_1:1;
then consider k being Nat such that
A3: n = (j + 1) + k by A2, NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take j ; :: thesis: ex k being Nat st
( n = (j + 1) + k & i = j + 1 )
take k ; :: thesis: ( n = (j + 1) + k & i = j + 1 )
thus ( n = (j + 1) + k & i = j + 1 ) by A2, A3; :: thesis: verum