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