( 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