let C be Cartesian_category; :: thesis: for a, b being Object of C holds <:(pr1 (a,b)),(pr2 (a,b)):> = id (a [x] b)
let a, b be Object of C; :: thesis: <:(pr1 (a,b)),(pr2 (a,b)):> = id (a [x] b)
A1: Hom ((a [x] b),b) <> {} by Th19;
then A2: (pr2 (a,b)) * (id (a [x] b)) = pr2 (a,b) by CAT_1:29;
A3: Hom ((a [x] b),a) <> {} by Th19;
then (pr1 (a,b)) * (id (a [x] b)) = pr1 (a,b) by CAT_1:29;
hence <:(pr1 (a,b)),(pr2 (a,b)):> = id (a [x] b) by A3, A1, A2, Def10; :: thesis: verum