let C be Cocartesian_category; :: thesis: for a being Object of C holds init a = init ((EmptyMS C),a)
let a be Object of C; :: thesis: init a = init ((EmptyMS C),a)
EmptyMS C is initial by Def26;
hence init a = init ((EmptyMS C),a) by CAT_3:40; :: thesis: verum