let C be Cocartesian_category; :: thesis: for a being Object of C holds
( dom (init a) = EmptyMS C & cod (init a) = a )
let a be Object of C; :: thesis: ( dom (init a) = EmptyMS C & cod (init a) = a )
( EmptyMS C is initial & init a = init ((EmptyMS C),a) ) by Def26, Th56;
hence ( dom (init a) = EmptyMS C & cod (init a) = a ) by CAT_3:38; :: thesis: verum