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 B * A is epi holds
B is epi
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 B * A is epi holds
B is epi )
assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: for A being Morphism of o1,o2
for B being Morphism of o2,o3 st B * A is epi holds
B is epi
let A be Morphism of o1,o2; :: thesis: for B being Morphism of o2,o3 st B * A is epi holds
B is epi
let B be Morphism of o2,o3; :: thesis: ( B * A is epi implies B is epi )
assume A2: B * A is epi ; :: thesis: B is epi
let o be Object of C; :: according to ALTCAT_3:def 8 :: thesis: ( <^o3,o^> <> {} implies for B, C being Morphism of o3,o st B * B = C * B holds
B = C )
assume A3: <^o3,o^> <> {} ; :: thesis: for B, C being Morphism of o3,o st B * B = C * B holds
B = C
let M1, M2 be Morphism of o3,o; :: thesis: ( M1 * B = M2 * B implies M1 = M2 )
assume A4: M1 * B = M2 * B ; :: thesis: M1 = M2
( (M1 * B) * A = M1 * (B * A) & (M2 * B) * A = M2 * (B * A) ) by A1, A3, ALTCAT_1:21;
hence M1 = M2 by A2, A3, A4; :: thesis: verum