let
a
be
Real
;
:: thesis:
for
n
being
Nat
holds
a
*
(
0*
n
)
=
0*
n
let
n
be
Nat
;
:: thesis:
a
*
(
0*
n
)
=
0*
n
|.
(
a
*
(
0*
n
)
)
.|
=
|.
a
.|
*
|.
(
0*
n
)
.|
by
EUCLID:11
.=
|.
a
.|
*
0
by
EUCLID:7
.=
0
;
hence
a
*
(
0*
n
)
=
0*
n
by
EUCLID:8
;
:: thesis:
verum