let C be category; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( M1 is _zero & M2 is _zero implies M2 * M1 is _zero )
assume that
A1: M1 is _zero and
A2: M2 is _zero ; :: thesis: M2 * M1 is _zero
let o be object of C; :: according to ALTCAT_3:def 12 :: thesis: ( 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 ; :: thesis: for A being Morphism of o1,o
for B being Morphism of o,o3 holds M2 * M1 = B * A
then A4: ( o is initial & o is terminal ) by Def11;
let A be Morphism of o1,o; :: thesis: for B being Morphism of o,o3 holds M2 * M1 = B * A
let B be Morphism of o,o3; :: thesis: M2 * M1 = B * A
consider B1 being Morphism of o,o2 such that
A5: ( B1 in <^o,o2^> & <^o,o2^> is trivial ) by A4, Def9;
consider B2 being Morphism of o,o3 such that
A6: ( B2 in <^o,o3^> & <^o,o3^> is trivial ) by A4, Def9;
consider A1 being Morphism of o1,o such that
A7: ( A1 in <^o1,o^> & <^o1,o^> is trivial ) by A4, Def10;
consider A2 being Morphism of o2,o such that
A8: ( A2 in <^o2,o^> & <^o2,o^> is trivial ) by A4, Def10;
A9: M2 = B2 * A2 by A2, A3, Def12;
consider x being set such that
A10: <^o1,o^> = {x} by A7, REALSET1:def 4;
A11: ( A = x & A1 = x ) by A10, TARSKI:def 1;
consider y being set such that
A12: <^o,o3^> = {y} by A6, REALSET1:def 4;
A13: ( B = y & B2 = y ) by A12, TARSKI:def 1;
ex M being Morphism of o,o st
( M in <^o,o^> & <^o,o^> is trivial ) by A4, Def10;
then consider z being set such that
A14: <^o,o^> = {z} by REALSET1:def 4;
A15: ( idm o = z & A2 * B1 = z ) by A14, TARSKI:def 1;
A16: ( <^o,o2^> <> {} & <^o2,o^> <> {} & <^o1,o^> <> {} & <^o,o3^> <> {} & <^o,o^> <> {} & <^o2,o3^> <> {} ) by A5, A6, A7, A8, ALTCAT_1:def 4;
thus M2 * M1 = (B2 * A2) * (B1 * A1) by A1, A3, A9, Def12
.= ((B2 * A2) * B1) * A1 by A16, ALTCAT_1:25
.= (B * (idm o)) * A by A5, A6, A8, A11, A13, A15, ALTCAT_1:25
.= B * A by A6, ALTCAT_1:def 19 ; :: thesis: verum