let C be Cocartesian_category; :: thesis: for a being Object of C holds Hom ((EmptyMS C),a) <> {}
let a be Object of C; :: thesis: Hom ((EmptyMS C),a) <> {}
EmptyMS C is initial by Def26;
hence Hom ((EmptyMS C),a) <> {} ; :: thesis: verum