let C be category; :: thesis: for o1, o2, o3 being Object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds
B is retraction
let o1, o2, o3 be Object of C; :: thesis: for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds
B is retraction
let A be Morphism of o1,o2; :: thesis: for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds
B is retraction
let B be Morphism of o2,o3; :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction implies B is retraction )
assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} ) ; :: thesis: ( not B * A is retraction or B is retraction )
assume B * A is retraction ; :: thesis: B is retraction
then consider G being Morphism of o3,o1 such that
A2: G is_right_inverse_of B * A ;
(B * A) * G = idm o3 by A2;
then B * (A * G) = idm o3 by A1, ALTCAT_1:21;
then A * G is_right_inverse_of B ;
hence B is retraction ; :: thesis: verum