for C1, C2 being category
for f being morphism of (C1 [x] C2) ex f1 being morphism of C1 ex f2 being morphism of C2 st f = [f1,f2]