let C be Category; :: thesis: for f being Morphism of C holds
( f is coretraction iff f opp is retraction )
let f be Morphism of C; :: thesis: ( f is coretraction iff f opp is retraction )
thus ( f is coretraction implies f opp is retraction ) :: thesis: ( f opp is retraction implies f is coretraction )

proof

given i being Morphism of C such that A1: dom i = cod f and
A2: i * f = id (dom f) ; :: according to CAT_3:def 9 :: thesis: f opp is retraction
take i opp ; :: according to CAT_3:def 8 :: thesis: ( cod (i opp) = dom (f opp) & (f opp) * (i opp) = id (cod (f opp)) )
thus cod (i opp) = cod f by A1, OPPCAT_1:8
.= dom (f opp) by OPPCAT_1:8 ; :: thesis: (f opp) * (i opp) = id (cod (f opp))
thus (f opp) * (i opp) = (id (dom f)) opp by A1, A2, OPPCAT_1:16
.= id ((dom f) opp) by OPPCAT_1:20
.= id (cod (f opp)) by OPPCAT_1:10 ; :: thesis: verum

end;

given i being Morphism of (C opp) such that A3: cod i = dom (f opp) and
A4: (f opp) * i = id (cod (f opp)) ; :: according to CAT_3:def 8 :: thesis: f is coretraction
take opp i ; :: according to CAT_3:def 9 :: thesis: ( dom (opp i) = cod f & (opp i) * f = id (dom f) )
thus A5: dom (opp i) = dom (f opp) by A3, OPPCAT_1:9
.= cod f by OPPCAT_1:8 ; :: thesis: (opp i) * f = id (dom f)
thus (opp i) * f = ((opp i) * f) opp by OPPCAT_1:def 4
.= (f opp) * ((opp i) opp) by A5, OPPCAT_1:16
.= id (cod (f opp)) by A4, OPPCAT_1:7
.= id ((dom f) opp) by OPPCAT_1:10
.= (id (dom f)) opp by OPPCAT_1:20
.= id (dom f) by OPPCAT_1:def 4 ; :: thesis: verum