let C1, C2 be category; :: thesis: for f being morphism of (C1 [x] C2) ex f1 being morphism of C1 ex f2 being morphism of C2 st f = [f1,f2]
let f be morphism of (C1 [x] C2); :: thesis: ex f1 being morphism of C1 ex f2 being morphism of C2 st f = [f1,f2]

per cases ( ( not C1 is empty & not C2 is empty ) or C1 is empty or C2 is empty ) ;

suppose A1: ( not C1 is empty & not C2 is empty ) ; :: thesis: ex f1 being morphism of C1 ex f2 being morphism of C2 st f = [f1,f2]

take (pr1 (C1,C2)) . f ; :: thesis: ex f2 being morphism of C2 st f = [((pr1 (C1,C2)) . f),f2]
take (pr2 (C1,C2)) . f ; :: thesis: f = [((pr1 (C1,C2)) . f),((pr2 (C1,C2)) . f)]
thus f = [((pr1 (C1,C2)) . f),((pr2 (C1,C2)) . f)] by A1, Def23; :: thesis: verum

end;

suppose A2: ( C1 is empty or C2 is empty ) ; :: thesis: ex f1 being morphism of C1 ex f2 being morphism of C2 st f = [f1,f2]

set f1 = the morphism of C1;
set f2 = the morphism of C2;
take the morphism of C1 ; :: thesis: ex f2 being morphism of C2 st f = [ the morphism of C1,f2]
take the morphism of C2 ; :: thesis: f = [ the morphism of C1, the morphism of C2]
f = {} by A2, SUBSET_1:def 1
.= the morphism of (C1 [x] C2) by A2, SUBSET_1:def 1 ;
hence f = [ the morphism of C1, the morphism of C2] by A2, Def23; :: thesis: verum

end;

end;