for C1, C2 being category
for f1 being morphism of C1
for f2 being morphism of C2
for f being morphism of (C1 [x] C2) st f = [f1,f2] & not C1 is empty & not C2 is empty holds
( f is identity iff ( f1 is identity & f2 is identity ) )