( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a ) by Th17;
hence pr1 (a,b) is Morphism of a [x] b,a by CAT_1:4; :: thesis: verum