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 coretraction holds
A is coretraction
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 coretraction holds
A is coretraction
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 coretraction holds
A is coretraction
let B be Morphism of o2,o3; :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction implies A is coretraction )
assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} ) ; :: thesis: ( not B * A is coretraction or A is coretraction )
assume B * A is coretraction ; :: thesis: A is coretraction
then consider G being Morphism of o3,o1 such that
A2: G is_left_inverse_of B * A ;
A3: (G * B) * A = G * (B * A) by A1, ALTCAT_1:21;
G * (B * A) = idm o1 by A2;
then G * B is_left_inverse_of A by A3;
hence A is coretraction ; :: thesis: verum