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