let
a
,
b
,
c
be
Integer
;
:: thesis:
(
a
divides
b
implies
a
divides
b
*
c
)
assume
a
divides
b
;
:: thesis:
a
divides
b
*
c
then
consider
l
being
Integer
such that
A1
:
b
=
a
*
l
;
(
a
*
l
)
*
c
=
a
*
(
l
*
c
)
;
hence
a
divides
b
*
c
by
A1
;
:: thesis:
verum