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