let n, k be Element of NAT ; :: thesis: ( k in Seg n iff ( k - 1 is Element of NAT & k - 1 < n ) )
A1: Seg n = { x where x is Nat : ( 1 <= x & x <= n ) } by FINSEQ_1:def 1;

hereby :: thesis: ( k - 1 is Element of NAT & k - 1 < n implies k in Seg n )

assume k in Seg n ; :: thesis: ( k - 1 is Element of NAT & k - 1 < n )
then consider x being Nat such that
A2: k = x and
A3: 1 <= x and
A4: x <= n by A1;
set x1 = k - 1;
set n1 = n - 1;
0 < x by A3;
then reconsider x1 = k - 1 as Element of NAT by A2, NAT_1:20;
x1 = k - 1 ;
hence k - 1 is Element of NAT ; :: thesis: k - 1 < n
0 < n by A3, A4;
then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
k + (- 1) <= n + (- 1) by A2, A4, XREAL_1:6;
then x1 <= n1 ;
then k - 1 < n1 + 1 by NAT_1:13;
hence k - 1 < n ; :: thesis: verum

end;

assume that
A5: k - 1 is Element of NAT and
A6: k - 1 < n ; :: thesis: k in Seg n
reconsider k1 = k - 1 as Element of NAT by A5;
0 <= k1 ;
then A7: 0 + 1 <= (k - 1) + 1 by XREAL_1:6;
(k - 1) + 1 <= (n - 1) + 1 by A5, A6, NAT_1:13;
hence k in Seg n by A1, A7; :: thesis: verum