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