let C be non empty transitive associative AltCatStr ; :: thesis: 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; :: thesis: ( <^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 A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: 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; :: thesis: 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; :: thesis: ( A is mono & B is mono implies B * A is mono )
assume A2: ( A is mono & B is mono ) ; :: thesis: B * A is mono
let o be object of C; :: according to ALTCAT_3:def 7 :: thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st (B * A) * B = (B * A) * C holds
B = C )
assume A3: <^o,o1^> <> {} ; :: thesis: for B, C being Morphism of o,o1 st (B * A) * B = (B * A) * C holds
B = C
let M1, M2 be Morphism of o,o1; :: thesis: ( (B * A) * M1 = (B * A) * M2 implies M1 = M2 )
assume A4: (B * A) * M1 = (B * A) * M2 ; :: thesis: M1 = M2
A5: (B * A) * M1 = B * (A * M1) by A1, A3, ALTCAT_1:25;
A6: (B * A) * M2 = B * (A * M2) by A1, A3, ALTCAT_1:25;
<^o,o2^> <> {} by A1, A3, ALTCAT_1:def 4;
then A * M1 = A * M2 by A2, A4, A5, A6, Def7;
hence M1 = M2 by A2, A3, Def7; :: thesis: verum