assume
A1
: (
a
=
c
&
b
=
d
) ;
:: thesis:
a
*
b
=
c
*
d
multint
.
(
a
,
b
) =
multreal
.
(
a
,
b
)
by
Def1
.=
c
*
d
by
A1
,
BINOP_2:def 11
;
hence
a
*
b
=
c
*
d
;
:: thesis:
verum