deffunc
H
_{1}
(
Element
of
INT.Ring
)
->
set
=
absreal
.
$1;
thus
for
f1
,
f2
being
Function
of
INT.Ring
,
NAT
st ( for
x
being
Element
of
INT.Ring
holds
f1
.
x
=
H
_{1}
(
x
) ) & ( for
x
being
Element
of
INT.Ring
holds
f2
.
x
=
H
_{1}
(
x
) ) holds
f1
=
f2
from
BINOP_2:sch 1
();
:: thesis:
verum