let
a
be
Element
of
multEX_0
;
:: thesis:
a
*
(
0.
multEX_0
)
=
0.
multEX_0
reconsider
aa
=
a
as
Real
;
thus
a
*
(
0.
multEX_0
)
=
aa
*
0
by
BINOP_2:def 11
.=
0.
multEX_0
;
:: thesis:
verum