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 ) )

hence id [c,d] = [(id c),(id d)] ; :: thesis: verum

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

then
m = id [c,d]
by CAT_1:def 12;
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 )

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;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 A8:
Hom (b,[c,d]) <> {}
; :: thesis: for f being Morphism of b,[c,d] holds [(id c),(id d)] (*) f = f
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;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

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

hence id [c,d] = [(id c),(id d)] ; :: thesis: verum