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

( 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