let C be non empty transitive associative AltCatStr ; for o1, o2, o3 being Object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is mono & B is mono holds
B * A is mono
let o1, o2, o3 be Object of C; ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is mono & B is mono holds
B * A is mono )
assume that
A1:
<^o1,o2^> <> {}
and
A2:
<^o2,o3^> <> {}
; for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is mono & B is mono holds
B * A is mono
let A be Morphism of o1,o2; for B being Morphism of o2,o3 st A is mono & B is mono holds
B * A is mono
let B be Morphism of o2,o3; ( A is mono & B is mono implies B * A is mono )
assume that
A3:
A is mono
and
A4:
B is mono
; B * A is mono
let o be Object of C; ALTCAT_3:def 7 ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st (B * A) * B = (B * A) * C holds
B = C )
assume A5:
<^o,o1^> <> {}
; for B, C being Morphism of o,o1 st (B * A) * B = (B * A) * C holds
B = C
then A6:
<^o,o2^> <> {}
by A1, ALTCAT_1:def 2;
let M1, M2 be Morphism of o,o1; ( (B * A) * M1 = (B * A) * M2 implies M1 = M2 )
assume A7:
(B * A) * M1 = (B * A) * M2
; M1 = M2
( (B * A) * M1 = B * (A * M1) & (B * A) * M2 = B * (A * M2) )
by A1, A2, A5, ALTCAT_1:21;
then
A * M1 = A * M2
by A4, A7, A6;
hence
M1 = M2
by A3, A5; verum