let
i
,
j
,
k
be
Integer
;
:: thesis:
(
i
divides
j
implies
k
*
i
divides
k
*
j
)
assume
i
divides
j
;
:: thesis:
k
*
i
divides
k
*
j
then
consider
z
being
Integer
such that
A1
:
i
*
z
=
j
by
INT_1:def 3
;
(
i
*
k
)
*
z
=
j
*
k
by
A1
;
hence
k
*
i
divides
k
*
j
by
INT_1:def 3
;
:: thesis:
verum