let C be non empty category; :: thesis: for a, b being Object of C

for f being Morphism of a,b st f is section_ holds

f is monomorphism

let a, b be Object of C; :: thesis: for f being Morphism of a,b st f is section_ holds

f is monomorphism

let f be Morphism of a,b; :: thesis: ( f is section_ implies f is monomorphism )

assume A1: f is section_ ; :: thesis: f is monomorphism

then consider g being Morphism of b,a such that

A2: g * f = id- a ;

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

g1 = g2

let c be Object of C; :: thesis: ( Hom (c,a) <> {} implies for g1, g2 being Morphism of c,a st f * g1 = f * g2 holds

g1 = g2 )

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

g1 = g2

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

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

A5: (g * f) * g1 = g * (f * g1) by A1, A3, Th23

.= (g * f) * g2 by A1, A4, A3, Th23 ;

thus g1 = (g * f) * g1 by A3, A2, Th18

.= g2 by A5, A3, A2, Th18 ; :: thesis: verum

for f being Morphism of a,b st f is section_ holds

f is monomorphism

let a, b be Object of C; :: thesis: for f being Morphism of a,b st f is section_ holds

f is monomorphism

let f be Morphism of a,b; :: thesis: ( f is section_ implies f is monomorphism )

assume A1: f is section_ ; :: thesis: f is monomorphism

then consider g being Morphism of b,a such that

A2: g * f = id- a ;

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

g1 = g2

let c be Object of C; :: thesis: ( Hom (c,a) <> {} implies for g1, g2 being Morphism of c,a st f * g1 = f * g2 holds

g1 = g2 )

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

g1 = g2

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

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

A5: (g * f) * g1 = g * (f * g1) by A1, A3, Th23

.= (g * f) * g2 by A1, A4, A3, Th23 ;

thus g1 = (g * f) * g1 by A3, A2, Th18

.= g2 by A5, A3, A2, Th18 ; :: thesis: verum