let k, n, i be natural number ; :: 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 i in Seg n ; :: thesis: k * i in Seg (k * n)
then A2: ( 1 <= i & i <= n ) by FINSEQ_1:3;
then A3: 1 * 1 <= k * i by A1, XREAL_1:68;
k * i <= k * n by A2, NAT_1:4;
hence k * i in Seg (k * n) by A3, FINSEQ_1:3; :: thesis: verum

end;

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