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