let C be non empty with_binary_products 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)
A1: Hom ((a [x] b),a) <> {} by Th42;
A2: ( Hom (a,a) <> {} & Hom (b,b) <> {} ) ;
A3: (id- a) * (pr1 (a,b)) = pr1 (a,b) by A1, CAT_7:18
.= (pr1 (a,b)) * (id- (a [x] b)) by A1, CAT_7:18 ;
A4: Hom ((a [x] b),b) <> {} by Th42;
(id- b) * (pr2 (a,b)) = pr2 (a,b) by A4, CAT_7:18
.= (pr2 (a,b)) * (id- (a [x] b)) by A4, CAT_7:18 ;
hence (id- a) [x] (id- b) = id- (a [x] b) by A2, A3, Def16; :: thesis: verum