let C be concrete category; for a, b being Object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is coretraction holds
f is one-to-one
let a, b be Object of C; ( <^a,b^> <> {} & <^b,a^> <> {} implies for f being Morphism of a,b st f is coretraction holds
f is one-to-one )
assume that
A1:
<^a,b^> <> {}
and
A2:
<^b,a^> <> {}
; for f being Morphism of a,b st f is coretraction holds
f is one-to-one
let f be Morphism of a,b; ( f is coretraction implies f is one-to-one )
given g being Morphism of b,a such that A3:
g is_left_inverse_of f
; ALTCAT_3:def 3 f is one-to-one
A4:
g * f = idm a
by A3;
A5:
g * f = g * f
by A1, A2, Th36;
A6:
dom f = the_carrier_of a
by A1, Th35;
idm a = id (the_carrier_of a)
by Def10;
hence
f is one-to-one
by A4, A5, A6, FUNCT_1:31; verum