theorem Th56: :: CAT_4:57

for C being Cocartesian_category
for a being Object of C holds init a = init ((EmptyMS C),a)