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