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