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),a <> {} & Hom (a [x] b),b <> {} ) by Th21;
then ( (pr1 a,b) * (id (a [x] b)) = pr1 a,b & (pr2 a,b) * (id (a [x] b)) = pr2 a,b ) by CAT_1:58;
hence <:(pr1 a,b),(pr2 a,b):> = id (a [x] b) by A1, Def11; :: thesis: verum