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 & cod (id a) = a ) by CAT_1:44;
then (id a) * (id a) = id a by CAT_1:47;
then A2: the Comp of A . (id a),(id a) = id a by A1, CAT_1:41;
[(id a),(id a)] in dom the Comp of A by A1, CAT_1:40;
hence [[(id a),(id a)],(id a)] in the Comp of A by A2, FUNCT_1:def 4; :: thesis: verum