theorem Th38: :: CAT_3:38

for C being Category
for a, b being Object of C st a is initial holds
( dom (init (a,b)) = a & cod (init (a,b)) = b )