let k, n, i be Nat; :: thesis: ( 1 <= k implies ( i in Seg n iff k * i in Seg (k * n) ) )
assume A1: 1 <= k ; :: thesis: ( i in Seg n iff k * i in Seg (k * n) )

hereby :: thesis: ( k * i in Seg (k * n) implies i in Seg n )

assume A2: i in Seg n ; :: thesis: k * i in Seg (k * n)
then i <= n by FINSEQ_1:1;
then A3: k * i <= k * n by NAT_1:4;
1 <= i by A2, FINSEQ_1:1;
then 1 * 1 <= k * i by A1, XREAL_1:66;
hence k * i in Seg (k * n) by A3, FINSEQ_1:1; :: thesis: verum

end;

assume A4: k * i in Seg (k * n) ; :: thesis: i in Seg n
then 0 < i by FINSEQ_1:1;
then A5: 0 + 1 <= i by NAT_1:13;
k * i <= k * n by A4, FINSEQ_1:1;
then i <= n by A1, XREAL_1:68;
hence i in Seg n by A5, FINSEQ_1:1; :: thesis: verum