let C1, C2 be category; :: thesis: (id C1) [x] (id C2) = id (C1 [x] C2)
A1: (id C1) (*) (pr1 (C1,C2)) = pr1 (C1,C2) by CAT_7:11
.= (pr1 (C1,C2)) (*) (id (C1 [x] C2)) by CAT_7:11 ;
(id C2) (*) (pr2 (C1,C2)) = pr2 (C1,C2) by CAT_7:11
.= (pr2 (C1,C2)) (*) (id (C1 [x] C2)) by CAT_7:11 ;
hence (id C1) [x] (id C2) = id (C1 [x] C2) by A1, Def22; :: thesis: verum