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