dom
(
chi
(
A
,
X
)
)
=
X
by
FUNCT_3:def 3
;
hence
chi
(
A
,
X
) is
Membership_Func
of
X
by
FUNCT_2:def 1
;
:: thesis:
verum