let C be Cocartesian_category; :: thesis: for a being Object of C holds init a = init ([0] C),a
let a be Object of C; :: thesis: init a = init ([0] C),a
[0] C is initial by Def27;
hence init a = init ([0] C),a by CAT_3:44; :: thesis: verum