let C be Category; for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,a) <> {} & g * f is retraction holds
g is retraction
let a, b, c be Object of C; for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,a) <> {} & g * f is retraction holds
g is retraction
let f be Morphism of a,b; for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,a) <> {} & g * f is retraction holds
g is retraction
let g be Morphism of b,c; ( Hom (a,b) <> {} & Hom (b,a) <> {} & g * f is retraction implies g is retraction )
assume A1:
( Hom (a,b) <> {} & Hom (b,a) <> {} )
; ( not g * f is retraction or g is retraction )
assume A2:
( Hom (a,c) <> {} & Hom (c,a) <> {} )
; CAT_3:def 8 ( for g being Morphism of c,a holds not (g * f) * g = id c or g is retraction )
given i being Morphism of c,a such that A3:
(g * f) * i = id c
; g is retraction
thus A4:
( Hom (b,c) <> {} & Hom (c,b) <> {} )
by A2, A1, CAT_1:24; CAT_3:def 8 ex g being Morphism of c,b st g * g = id c
take
f * i
; g * (f * i) = id c
thus
g * (f * i) = id c
by A2, A3, A4, A1, CAT_1:25; verum