x
in
{
x
}
by
TARSKI:def 1
;
then
x
in
dom
(
{
x
}
-->
y
)
;
then
A1
:
x
in
dom
(
x
.-->
y
)
by
FUNCOP_1:def 9
;
(
x
is
set
&
y
is
set
)
by
TARSKI:1
;
hence
proj
(
(
x
.-->
y
)
,
x
) is
one-to-one
by
A1
,
Th19
;
:: thesis:
verum