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;

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

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 that 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;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

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