deffunc
H
_{1}
(
Element
of
[:
A
,
B
:]
)
->
Element
of
[:
B
,
A
:]
=
[
(
$1
`2
)
,
(
$1
`1
)
]
;
thus
ex
I
being
Function
of
[:
A
,
B
:]
,
[:
B
,
A
:]
st
for
a
being
Element
of
[:
A
,
B
:]
holds
I
.
a
=
H
_{1}
(
a
)
from
FUNCT_2:sch 4
();
:: thesis:
verum