set
p
=
a
.-->
b
;
(
dom
(
a
.-->
b
)
=
{
a
}
&
rng
(
a
.-->
b
)
=
{
b
}
)
by
FUNCOP_1:8
;
then
(
dom
(
a
.-->
b
)
c=
X
&
rng
(
a
.-->
b
)
c=
Y
) ;
hence
a
.-->
b
is
PartFunc
of
X
,
Y
by
RELSET_1:4
;
:: thesis:
verum