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