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 coretraction & B is coretraction holds
B * A is coretraction
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 coretraction & B is coretraction holds
B * A is coretraction )
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 coretraction & B is coretraction holds
B * A is coretraction
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 coretraction & B is coretraction holds
B * A is coretraction
let B be Morphism of o2,o3; :: thesis: ( A is coretraction & B is coretraction implies B * A is coretraction )
assume A3: ( A is coretraction & B is coretraction ) ; :: thesis: B * A is coretraction
then consider A1 being Morphism of o2,o1 such that
A4: A1 is_left_inverse_of A by Def3;
consider B1 being Morphism of o3,o2 such that
A5: B1 is_left_inverse_of B by A3, Def3;
consider G being Morphism of o3,o1 such that
A6: G = A1 * B1 ;
take G ; :: according to ALTCAT_3:def 3 :: thesis: G is_left_inverse_of B * A
A7: <^o2,o2^> <> {} by ALTCAT_1:23;
G * (B * A) = ((A1 * B1) * B) * A by A1, A6, ALTCAT_1:25
.= (A1 * (B1 * B)) * A by A1, A2, ALTCAT_1:25
.= (A1 * (idm o2)) * A by A5, Def1
.= A1 * ((idm o2) * A) by A1, A2, A7, ALTCAT_1:25
.= A1 * A by A1, ALTCAT_1:24
.= idm o1 by A4, Def1 ;
hence G is_left_inverse_of B * A by Def1; :: thesis: verum