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