take f = X --> (1Cat ({},{{}})); :: thesis: f is Category-yielding
let x be set ; :: according to INDEX_1:def 1 :: thesis: ( x in dom f implies f . x is Category )
assume x in dom f ; :: thesis: f . x is Category
then x in X ;
hence f . x is Category by FUNCOP_1:7; :: thesis: verum