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:38; :: thesis: verum