let C be Cocartesian_category; :: thesis: for a being Object of C
for f1, f2 being Morphism of [[0]] C,a holds f1 = f2
let a be Object of C; :: thesis: for f1, f2 being Morphism of [[0]] C,a holds f1 = f2
let f1, f2 be Morphism of [[0]] C,a; :: thesis: f1 = f2
[[0]] C is initial by Def27;
then consider f being Morphism of [[0]] C,a such that
A1: for g being Morphism of [[0]] C,a holds f = g by CAT_1:def 13;
thus f1 = f by A1
.= f2 by A1 ; :: thesis: verum