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