let A be Category; :: thesis: for a being Object of A holds [[(id a),(id a)],(id a)] in the Comp of A
let a be Object of A; :: thesis: [[(id a),(id a)],(id a)] in the Comp of A
A1: dom (id a) = a ;
A2: cod (id a) = a ;
then A3: [(id a),(id a)] in dom the Comp of A by A1, CAT_1:15;
(id a) (*) (id a) = id a by A1, CAT_1:22;
then the Comp of A . ((id a),(id a)) = id a by A1, A2, CAT_1:16;
hence [[(id a),(id a)],(id a)] in the Comp of A by A3, FUNCT_1:def 2; :: thesis: verum