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