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