set
x
= the
Element
of
Z
;
A1
:
dom
f
=
X
by
FUNCT_2:def 1
;
thus
not
f
.:
Z
is
empty
by
A1
;
:: thesis:
verum