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