let C be category; :: thesis: for a, b, c being Object of C
for f1 being Morphism of a,b
for f2 being Morphism of b,c st f1 is monomorphism & f2 is monomorphism holds
f2 * f1 is monomorphism
let a, b, c be Object of C; :: thesis: for f1 being Morphism of a,b
for f2 being Morphism of b,c st f1 is monomorphism & f2 is monomorphism holds
f2 * f1 is monomorphism
let f1 be Morphism of a,b; :: thesis: for f2 being Morphism of b,c st f1 is monomorphism & f2 is monomorphism holds
f2 * f1 is monomorphism
let f2 be Morphism of b,c; :: thesis: ( f1 is monomorphism & f2 is monomorphism implies f2 * f1 is monomorphism )
assume A1: f1 is monomorphism ; :: thesis: ( not f2 is monomorphism or f2 * f1 is monomorphism )
assume A2: f2 is monomorphism ; :: thesis: f2 * f1 is monomorphism
hence Hom (a,c) <> {} by A1, Th22; :: according to CAT_7:def 5 :: thesis: for c being Object of C st Hom (c,a) <> {} holds
for g1, g2 being Morphism of c,a st (f2 * f1) * g1 = (f2 * f1) * g2 holds
g1 = g2
let d be Object of C; :: thesis: ( Hom (d,a) <> {} implies for g1, g2 being Morphism of d,a st (f2 * f1) * g1 = (f2 * f1) * g2 holds
g1 = g2 )
assume A3: Hom (d,a) <> {} ; :: thesis: for g1, g2 being Morphism of d,a st (f2 * f1) * g1 = (f2 * f1) * g2 holds
g1 = g2
let g1, g2 be Morphism of d,a; :: thesis: ( (f2 * f1) * g1 = (f2 * f1) * g2 implies g1 = g2 )
assume A4: (f2 * f1) * g1 = (f2 * f1) * g2 ; :: thesis: g1 = g2
A5: Hom (d,b) <> {} by A3, A1, Th22;
f2 * (f1 * g1) = (f2 * f1) * g1 by A1, A2, A3, Th23
.= f2 * (f1 * g2) by A4, A1, A2, A3, Th23 ;
hence g1 = g2 by A1, A3, A2, A5; :: thesis: verum