let C be Category; :: thesis: for a, b being Object of C

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

f is monic

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

f is monic

let f be Morphism of a,b; :: thesis: ( f is coretraction implies f is monic )

assume A1: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_3:def 9 :: thesis: ( for g being Morphism of b,a holds not g * f = id a or f is monic )

given g being Morphism of b,a such that A2: g * f = id a ; :: thesis: f is monic

thus Hom (a,b) <> {} by A1; :: according to CAT_1:def 14 :: thesis: for b_{1} being Element of the carrier of C holds

( Hom (b_{1},a) = {} or for b_{2}, b_{3} being Morphism of b_{1},a holds

( not f * b_{2} = f * b_{3} or b_{2} = b_{3} ) )

let c be Object of C; :: thesis: ( Hom (c,a) = {} or for b_{1}, b_{2} being Morphism of c,a holds

( not f * b_{1} = f * b_{2} or b_{1} = b_{2} ) )

assume A3: Hom (c,a) <> {} ; :: thesis: for b_{1}, b_{2} being Morphism of c,a holds

( not f * b_{1} = f * b_{2} or b_{1} = b_{2} )

let p1, p2 be Morphism of c,a; :: thesis: ( not f * p1 = f * p2 or p1 = p2 )

assume A4: f * p1 = f * p2 ; :: thesis: p1 = p2

thus p1 = (g * f) * p1 by A3, A2, CAT_1:28

.= g * (f * p2) by A3, A1, A4, CAT_1:25

.= (g * f) * p2 by A3, A1, CAT_1:25

.= p2 by A3, A2, CAT_1:28 ; :: thesis: verum

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

f is monic

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

f is monic

let f be Morphism of a,b; :: thesis: ( f is coretraction implies f is monic )

assume A1: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_3:def 9 :: thesis: ( for g being Morphism of b,a holds not g * f = id a or f is monic )

given g being Morphism of b,a such that A2: g * f = id a ; :: thesis: f is monic

thus Hom (a,b) <> {} by A1; :: according to CAT_1:def 14 :: thesis: for b

( Hom (b

( not f * b

let c be Object of C; :: thesis: ( Hom (c,a) = {} or for b

( not f * b

assume A3: Hom (c,a) <> {} ; :: thesis: for b

( not f * b

let p1, p2 be Morphism of c,a; :: thesis: ( not f * p1 = f * p2 or p1 = p2 )

assume A4: f * p1 = f * p2 ; :: thesis: p1 = p2

thus p1 = (g * f) * p1 by A3, A2, CAT_1:28

.= g * (f * p2) by A3, A1, A4, CAT_1:25

.= (g * f) * p2 by A3, A1, CAT_1:25

.= p2 by A3, A2, CAT_1:28 ; :: thesis: verum