let C be category; :: thesis: for o1, o2 being object of C
for m, m' being Morphism of o1,o2 st m is _zero & m' is _zero & ex O being object of C st O is _zero holds
m = m'
let o1, o2 be object of C; :: thesis: for m, m' being Morphism of o1,o2 st m is _zero & m' is _zero & ex O being object of C st O is _zero holds
m = m'
let m, m' be Morphism of o1,o2; :: thesis: ( m is _zero & m' is _zero & ex O being object of C st O is _zero implies m = m' )
assume that
A1: m is _zero and
A2: m' is _zero ; :: thesis: ( for O being object of C holds not O is _zero or m = m' )
given O being object of C such that A3: O is _zero ; :: thesis: m = m'
consider a being Morphism of o1,O;
consider b being Morphism of O,o2;
consider n being Morphism of O,O;
thus m = (b * ((n " ) * n)) * a by A1, A3, ALTCAT_3:def 12
.= m' by A2, A3, ALTCAT_3:def 12 ; :: thesis: verum