let C be category; :: thesis: for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is retraction & B is retraction holds
B * A is retraction
let o1, o2, o3 be object of C; :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} implies for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is retraction & B is retraction holds
B * A is retraction )
assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} ) ; :: thesis: for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is retraction & B is retraction holds
B * A is retraction
then A2: ( <^o2,o1^> <> {} & <^o3,o2^> <> {} & <^o1,o3^> <> {} ) by ALTCAT_1:def 4;
let A be Morphism of o1,o2; :: thesis: for B being Morphism of o2,o3 st A is retraction & B is retraction holds
B * A is retraction
let B be Morphism of o2,o3; :: thesis: ( A is retraction & B is retraction implies B * A is retraction )
assume A3: ( A is retraction & B is retraction ) ; :: thesis: B * A is retraction
then consider A1 being Morphism of o2,o1 such that
A4: A1 is_right_inverse_of A by Def2;
consider B1 being Morphism of o3,o2 such that
A5: B1 is_right_inverse_of B by A3, Def2;
consider G being Morphism of o3,o1 such that
A6: G = A1 * B1 ;
take G ; :: according to ALTCAT_3:def 2 :: thesis: G is_right_inverse_of B * A
(B * A) * G = B * (A * (A1 * B1)) by A1, A6, ALTCAT_1:25
.= B * ((A * A1) * B1) by A1, A2, ALTCAT_1:25
.= B * ((idm o2) * B1) by A4, Def1
.= B * B1 by A2, ALTCAT_1:24
.= idm o3 by A5, Def1 ;
hence G is_right_inverse_of B * A by Def1; :: thesis: verum