let a be set ; :: according to INDEX_1:def 1 :: thesis: ( a in dom (X --> x) implies (X --> x) . a is Category )
assume a in dom (X --> x) ; :: thesis: (X --> x) . a is Category
then a in X by FUNCOP_1:13;
hence (X --> x) . a is Category by FUNCOP_1:7; :: thesis: verum