let C be Category; :: thesis: for f being Morphism of C st f is coretraction holds
f is monic
let f be Morphism of C; :: thesis: ( f is coretraction implies f is monic )
given g being Morphism of C such that A1: dom g = cod f and
A2: g * f = id (dom f) ; :: according to CAT_3:def 11 :: thesis: f is monic
let p1 be Morphism of C; :: according to CAT_1:def 10 :: thesis: for b₁ being Element of the carrier' of C holds
( not dom p1 = dom b₁ or not cod p1 = dom f or not cod b₁ = dom f or not f * p1 = f * b₁ or p1 = b₁ )
let p2 be Morphism of C; :: thesis: ( not dom p1 = dom p2 or not cod p1 = dom f or not cod p2 = dom f or not f * p1 = f * p2 or p1 = p2 )
assume that
dom p1 = dom p2 and
A3: cod p1 = dom f and
A4: cod p2 = dom f and
A5: f * p1 = f * p2 ; :: thesis: p1 = p2
thus p1 = (g * f) * p1 by A2, A3, CAT_1:46
.= g * (f * p2) by A1, A3, A5, CAT_1:43
.= (g * f) * p2 by A1, A4, CAT_1:43
.= p2 by A2, A4, CAT_1:46 ; :: thesis: verum