let C be Cocartesian_category; :: thesis: for a being Object of C holds Hom ([[0]] C),a = {(init a)}
let a be Object of C; :: thesis: Hom ([[0]] C),a = {(init a)}
for f2 being Morphism of [[0]] C,a holds init a = f2 by Th59;
hence Hom ([[0]] C),a = {(init a)} by Th60, CAT_1:26; :: thesis: verum