let C be category; :: thesis: for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is coretraction holds
A is mono
let o1, o2 be object of C; :: thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is coretraction holds
A is mono )
assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; :: thesis: for A being Morphism of o1,o2 st A is coretraction holds
A is mono
let A be Morphism of o1,o2; :: thesis: ( A is coretraction implies A is mono )
assume A is coretraction ; :: thesis: A is mono
then consider R being Morphism of o2,o1 such that
A2: R is_left_inverse_of A by Def3;
let o be object of C; :: according to ALTCAT_3:def 7 :: thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds
B = C )
assume A3: <^o,o1^> <> {} ; :: thesis: for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
let B, C be Morphism of o,o1; :: thesis: ( A * B = A * C implies B = C )
assume A4: A * B = A * C ; :: thesis: B = C
thus B = (idm o1) * B by A3, ALTCAT_1:24
.= (R * A) * B by A2, Def1
.= R * (A * C) by A1, A3, A4, ALTCAT_1:25
.= (R * A) * C by A1, A3, ALTCAT_1:25
.= (idm o1) * C by A2, Def1
.= C by A3, ALTCAT_1:24 ; :: thesis: verum