let C be Cocartesian_category; :: thesis: for a being Object of C holds Hom ((EmptyMS C),a) = {(init a)}
let a be Object of C; :: thesis: Hom ((EmptyMS C),a) = {(init a)}
for f2 being Morphism of EmptyMS C,a holds init a = f2 by Th54;
hence Hom ((EmptyMS C),a) = {(init a)} by Th55, CAT_1:8; :: thesis: verum