deffunc
H
_{1}
(
Element
of
[:
(
Fin
A
)
,
(
Fin
A
)
:]
,
Element
of
[:
(
Fin
A
)
,
(
Fin
A
)
:]
)
->
Element
of
[:
(
Fin
A
)
,
(
Fin
A
)
:]
= $1
\
$2;
thus
ex
f
being
BinOp
of
[:
(
Fin
A
)
,
(
Fin
A
)
:]
st
for
a
,
b
being
Element
of
[:
(
Fin
A
)
,
(
Fin
A
)
:]
holds
f
.
(
a
,
b
)
=
H
_{1}
(
a
,
b
)
from
BINOP_1:sch 4
();
:: thesis:
verum