deffunc
H
_{1}
(
NatPlus
,
NatPlus
)
->
Element
of
omega
= $1
gcd
$2;
thus
for
o1
,
o2
being
BinOp
of
NATPLUS
st ( for
a
,
b
being
NatPlus
holds
o1
.
(
a
,
b
)
=
H
_{1}
(
a
,
b
) ) & ( for
a
,
b
being
NatPlus
holds
o2
.
(
a
,
b
)
=
H
_{1}
(
a
,
b
) ) holds
o1
=
o2
from
BINOP_2:sch 2
();
:: thesis:
verum