deffunc
H
_{1}
(
Element
of
A
)
->
object
=
[
$1,
y
]
;
thus
for
f1
,
f2
being
Function
of
A
,
[:
A
,
B
:]
st ( for
x
being
Element
of
A
holds
f1
.
x
=
H
_{1}
(
x
) ) & ( for
x
being
Element
of
A
holds
f2
.
x
=
H
_{1}
(
x
) ) holds
f1
=
f2
from
BINOP_2:sch 1
();
:: thesis:
verum