let C be Cocartesian_category; :: thesis: for a being Object of C holds
( dom (init a) = [0] C & cod (init a) = a )
let a be Object of C; :: thesis: ( dom (init a) = [0] C & cod (init a) = a )
( [0] C is initial & init a = init ([0] C),a ) by Def27, Th61;
hence ( dom (init a) = [0] C & cod (init a) = a ) by CAT_3:42; :: thesis: verum