let C be Cocartesian_category; :: thesis: for a being Object of C
for f1, f2 being Morphism of EmptyMS C,a holds f1 = f2
let a be Object of C; :: thesis: for f1, f2 being Morphism of EmptyMS C,a holds f1 = f2
let f1, f2 be Morphism of EmptyMS C,a; :: thesis: f1 = f2
EmptyMS C is initial by Def26;
then consider f being Morphism of EmptyMS C,a such that
A1: for g being Morphism of EmptyMS C,a holds f = g ;
thus f1 = f by A1
.= f2 by A1 ; :: thesis: verum