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

for f being Morphism of a,b

for g being Morphism of b,c st f is retraction & g is retraction holds

g * f is retraction

let a, b, c be Object of C; :: thesis: for f being Morphism of a,b

for g being Morphism of b,c st f is retraction & g is retraction holds

g * f is retraction

let f be Morphism of a,b; :: thesis: for g being Morphism of b,c st f is retraction & g is retraction holds

g * f is retraction

let g be Morphism of b,c; :: thesis: ( f is retraction & g is retraction implies g * f is retraction )

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

given i being Morphism of b,a such that A2: f * i = id b ; :: thesis: ( not g is retraction or g * f is retraction )

assume A3: ( Hom (b,c) <> {} & Hom (c,b) <> {} ) ; :: according to CAT_3:def 8 :: thesis: ( for g being Morphism of c,b holds not g * g = id c or g * f is retraction )

given j being Morphism of c,b such that A4: g * j = id c ; :: thesis: g * f is retraction

thus A5: ( Hom (a,c) <> {} & Hom (c,a) <> {} ) by A1, A3, CAT_1:24; :: according to CAT_3:def 8 :: thesis: ex g being Morphism of c,a st (g * f) * g = id c

take i * j ; :: thesis: (g * f) * (i * j) = id c

thus (g * f) * (i * j) = g * (f * (i * j)) by A1, A3, A5, CAT_1:25

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

.= id c by A2, A3, A4, CAT_1:28 ; :: thesis: verum

for f being Morphism of a,b

for g being Morphism of b,c st f is retraction & g is retraction holds

g * f is retraction

let a, b, c be Object of C; :: thesis: for f being Morphism of a,b

for g being Morphism of b,c st f is retraction & g is retraction holds

g * f is retraction

let f be Morphism of a,b; :: thesis: for g being Morphism of b,c st f is retraction & g is retraction holds

g * f is retraction

let g be Morphism of b,c; :: thesis: ( f is retraction & g is retraction implies g * f is retraction )

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

given i being Morphism of b,a such that A2: f * i = id b ; :: thesis: ( not g is retraction or g * f is retraction )

assume A3: ( Hom (b,c) <> {} & Hom (c,b) <> {} ) ; :: according to CAT_3:def 8 :: thesis: ( for g being Morphism of c,b holds not g * g = id c or g * f is retraction )

given j being Morphism of c,b such that A4: g * j = id c ; :: thesis: g * f is retraction

thus A5: ( Hom (a,c) <> {} & Hom (c,a) <> {} ) by A1, A3, CAT_1:24; :: according to CAT_3:def 8 :: thesis: ex g being Morphism of c,a st (g * f) * g = id c

take i * j ; :: thesis: (g * f) * (i * j) = id c

thus (g * f) * (i * j) = g * (f * (i * j)) by A1, A3, A5, CAT_1:25

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

.= id c by A2, A3, A4, CAT_1:28 ; :: thesis: verum