let
X
,
Y
be
set
;
:: thesis:
for
f
being
Function
of
[:
X
,
Y
:]
,
Y
holds
dom
f
=
[:
X
,
Y
:]
let
f
be
Function
of
[:
X
,
Y
:]
,
Y
;
:: thesis:
dom
f
=
[:
X
,
Y
:]
(
Y
is
empty
implies
[:
X
,
Y
:]
is
empty
)
by
ZFMISC_1:90
;
hence
dom
f
=
[:
X
,
Y
:]
by
FUNCT_2:def 1
;
:: thesis:
verum