theorem :: CAT_2:27
for C, D being Category
for fg being Morphism of [:C,D:] ex f being Morphism of C ex g being Morphism of D st fg = [f,g] by DOMAIN_1:1;