let x be set ; :: according to INDEX_1:def 1 :: thesis: ( x in dom (g * f) implies (g * f) . x is Category )
assume x in dom (g * f) ; :: thesis: (g * f) . x is Category
then ( (g * f) . x = g . (f . x) & f . x in dom g ) by FUNCT_1:11, FUNCT_1:12;
hence (g * f) . x is Category by Def1; :: thesis: verum