take f = {} --> (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
hence f . x is Category ; :: thesis: verum