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 by Def2;
(B * A) * G = idm o3 by A2, Def1;
then B * (A * G) = idm o3 by A1, ALTCAT_1:25;
then A * G is_right_inverse_of B by Def1;
then consider F being Morphism of o3,o2 such that
A3: ( F = A * G & F is_right_inverse_of B ) ;
thus B is retraction by A3, Def2; :: thesis: verum