let C, D be Category; :: thesis: for c being Object of C
for d being Object of D holds id [c,d] = [(id c),(id d)]
let c be Object of C; :: thesis: for d being Object of D holds id [c,d] = [(id c),(id d)]
let d be Object of D; :: thesis: id [c,d] = [(id c),(id d)]
A1: dom [(id c),(id d)] = [(dom (id c)),(dom (id d))] by Th22
.= [c,(dom (id d))]
.= [c,d] ;
cod [(id c),(id d)] = [(cod (id c)),(cod (id d))] by Th22
.= [c,(cod (id d))]
.= [c,d] ;
then reconsider m = [(id c),(id d)] as Morphism of [c,d],[c,d] by A1, CAT_1:4;
for b being Object of [:C,D:] holds
( ( Hom ([c,d],b) <> {} implies for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f ) & ( Hom (b,[c,d]) <> {} implies for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f ) )

proof

let b be Object of [:C,D:]; :: thesis: ( ( Hom ([c,d],b) <> {} implies for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f ) & ( Hom (b,[c,d]) <> {} implies for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f ) )
thus ( Hom ([c,d],b) <> {} implies for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f ) :: thesis: ( Hom (b,[c,d]) <> {} implies for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f )

proof

assume A2: Hom ([c,d],b) <> {} ; :: thesis: for f being Morphism of [c,d],b holds f (*) [(id c),(id d)] = f
let f be Morphism of [c,d],b; :: thesis: f (*) [(id c),(id d)] = f
consider fc being Morphism of C, fd being Morphism of D such that
A3: f = [fc,fd] by DOMAIN_1:1;
A4: [c,d] = dom f by A2, CAT_1:5
.= [(dom fc),(dom fd)] by A3, Th22 ;
then A5: c = dom fc by XTUPLE_0:1;
then A6: cod (id c) = dom fc ;
A7: d = dom fd by A4, XTUPLE_0:1;
then cod (id d) = dom fd ;
hence f (*) [(id c),(id d)] = [(fc (*) (id c)),(fd (*) (id d))] by A3, A6, Th23
.= [fc,(fd (*) (id d))] by A5, CAT_1:22
.= f by A3, A7, CAT_1:22 ;
:: thesis: verum

end;

assume A8: Hom (b,[c,d]) <> {} ; :: thesis: for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f
let f be Morphism of b,[c,d]; :: thesis: [(id c),(id d)] (*) f = f
consider fc being Morphism of C, fd being Morphism of D such that
A9: f = [fc,fd] by DOMAIN_1:1;
A10: [c,d] = cod f by A8, CAT_1:5
.= [(cod fc),(cod fd)] by A9, Th22 ;
then A11: c = cod fc by XTUPLE_0:1;
then A12: dom (id c) = cod fc ;
A13: d = cod fd by A10, XTUPLE_0:1;
then dom (id d) = cod fd ;
hence [(id c),(id d)] (*) f = [((id c) (*) fc),((id d) (*) fd)] by A9, A12, Th23
.= [fc,((id d) (*) fd)] by A11, CAT_1:21
.= f by A9, A13, CAT_1:21 ;
:: thesis: verum

end;

then m = id [c,d] by CAT_1:def 12;
hence id [c,d] = [(id c),(id d)] ; :: thesis: verum