let C be category; :: thesis: for o1, o2, o3 being object of
for A being Morphism of ,
for B being Morphism of , st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds
B is retraction
let o1, o2, o3 be object of ; :: thesis: for A being Morphism of ,
for B being Morphism of , st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds
B is retraction
let A be Morphism of ,; :: thesis: for B being Morphism of , st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds
B is retraction
let B be Morphism of ,; :: 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 , 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;
hence B is retraction by Def2; :: thesis: verum