let C be category; for o1, o2, o3 being Object of C
for M1 being Morphism of o1,o2
for M2 being Morphism of o2,o3 st M1 is _zero & M2 is _zero holds
M2 * M1 is _zero
let o1, o2, o3 be Object of C; for M1 being Morphism of o1,o2
for M2 being Morphism of o2,o3 st M1 is _zero & M2 is _zero holds
M2 * M1 is _zero
let M1 be Morphism of o1,o2; for M2 being Morphism of o2,o3 st M1 is _zero & M2 is _zero holds
M2 * M1 is _zero
let M2 be Morphism of o2,o3; ( M1 is _zero & M2 is _zero implies M2 * M1 is _zero )
assume that
A1:
M1 is _zero
and
A2:
M2 is _zero
; M2 * M1 is _zero
let o be Object of C; ALTCAT_3:def 12 ( o is _zero implies for A being Morphism of o1,o
for B being Morphism of o,o3 holds M2 * M1 = B * A )
assume A3:
o is _zero
; for A being Morphism of o1,o
for B being Morphism of o,o3 holds M2 * M1 = B * A
then A4:
o is initial
;
then consider B1 being Morphism of o,o2 such that
A5:
B1 in <^o,o2^>
and
<^o,o2^> is trivial
;
let A be Morphism of o1,o; for B being Morphism of o,o3 holds M2 * M1 = B * A
let B be Morphism of o,o3; M2 * M1 = B * A
consider B2 being Morphism of o,o3 such that
A6:
B2 in <^o,o3^>
and
A7:
<^o,o3^> is trivial
by A4;
consider y being object such that
A8:
<^o,o3^> = {y}
by A6, A7, ZFMISC_1:131;
A9:
o is terminal
by A3;
then consider A1 being Morphism of o1,o such that
A10:
A1 in <^o1,o^>
and
A11:
<^o1,o^> is trivial
;
consider x being object such that
A12:
<^o1,o^> = {x}
by A10, A11, ZFMISC_1:131;
ex M being Morphism of o,o st
( M in <^o,o^> & <^o,o^> is trivial )
by A9;
then consider z being object such that
A13:
<^o,o^> = {z}
by ZFMISC_1:131;
consider A2 being Morphism of o2,o such that
A14:
A2 in <^o2,o^>
and
<^o2,o^> is trivial
by A9;
A15:
( idm o = z & A2 * B1 = z )
by A13, TARSKI:def 1;
A16:
( B = y & B2 = y )
by A8, TARSKI:def 1;
A17:
( A = x & A1 = x )
by A12, TARSKI:def 1;
A18:
<^o2,o3^> <> {}
by A6, A14, ALTCAT_1:def 2;
M2 = B2 * A2
by A2, A3;
hence M2 * M1 =
(B2 * A2) * (B1 * A1)
by A1, A3
.=
((B2 * A2) * B1) * A1
by A5, A10, A18, ALTCAT_1:21
.=
(B * (idm o)) * A
by A5, A6, A14, A17, A16, A15, ALTCAT_1:21
.=
B * A
by A6, ALTCAT_1:def 17
;
verum