let C be Cocartesian_category; :: thesis: for a being Object of C holds Hom ([[0]] C),a <> {}
let a be Object of C; :: thesis: Hom ([[0]] C),a <> {}
[[0]] C is initial by Def27;
hence Hom ([[0]] C),a <> {} by CAT_1:def 16; :: thesis: verum