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 f2 * f1 is monomorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds

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 f2 * f1 is monomorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds

f1 is monomorphism

let f1 be Morphism of a,b; :: thesis: for f2 being Morphism of b,c st f2 * f1 is monomorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds

f1 is monomorphism

let f2 be Morphism of b,c; :: thesis: ( f2 * f1 is monomorphism & Hom (a,b) <> {} & Hom (b,c) <> {} implies f1 is monomorphism )

assume A1: f2 * f1 is monomorphism ; :: thesis: ( not Hom (a,b) <> {} or not Hom (b,c) <> {} or f1 is monomorphism )

assume A2: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ; :: thesis: f1 is monomorphism

thus Hom (a,b) <> {} by A2; :: 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 f1 * g1 = 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 f1 * g1 = f1 * g2 holds

g1 = g2 )

assume A3: Hom (d,a) <> {} ; :: thesis: for g1, g2 being Morphism of d,a st f1 * g1 = f1 * g2 holds

g1 = g2

let g1, g2 be Morphism of d,a; :: thesis: ( f1 * g1 = f1 * g2 implies g1 = g2 )

assume A4: f1 * g1 = f1 * g2 ; :: thesis: g1 = g2

(f2 * f1) * g1 = f2 * (f1 * g1) by A2, A3, Th23

.= (f2 * f1) * g2 by A2, A4, A3, Th23 ;

hence g1 = g2 by A1, A3; :: thesis: verum

for f1 being Morphism of a,b

for f2 being Morphism of b,c st f2 * f1 is monomorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds

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 f2 * f1 is monomorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds

f1 is monomorphism

let f1 be Morphism of a,b; :: thesis: for f2 being Morphism of b,c st f2 * f1 is monomorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds

f1 is monomorphism

let f2 be Morphism of b,c; :: thesis: ( f2 * f1 is monomorphism & Hom (a,b) <> {} & Hom (b,c) <> {} implies f1 is monomorphism )

assume A1: f2 * f1 is monomorphism ; :: thesis: ( not Hom (a,b) <> {} or not Hom (b,c) <> {} or f1 is monomorphism )

assume A2: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ; :: thesis: f1 is monomorphism

thus Hom (a,b) <> {} by A2; :: 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 f1 * g1 = 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 f1 * g1 = f1 * g2 holds

g1 = g2 )

assume A3: Hom (d,a) <> {} ; :: thesis: for g1, g2 being Morphism of d,a st f1 * g1 = f1 * g2 holds

g1 = g2

let g1, g2 be Morphism of d,a; :: thesis: ( f1 * g1 = f1 * g2 implies g1 = g2 )

assume A4: f1 * g1 = f1 * g2 ; :: thesis: g1 = g2

(f2 * f1) * g1 = f2 * (f1 * g1) by A2, A3, Th23

.= (f2 * f1) * g2 by A2, A4, A3, Th23 ;

hence g1 = g2 by A1, A3; :: thesis: verum