let C be category; :: thesis: ( ( for o1, o2 being Object of C

for f being Morphism of o1,o2 holds f is coretraction ) implies for a, b being Object of C

for g being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds

g is iso )

assume A1: for o1, o2 being Object of C

for f being Morphism of o1,o2 holds f is coretraction ; :: thesis: for a, b being Object of C

for g being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds

g is iso

let a, b be Object of C; :: thesis: for g being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds

g is iso

let g be Morphism of a,b; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies g is iso )

assume that

A2: <^a,b^> <> {} and

A3: <^b,a^> <> {} ; :: thesis: g is iso

A4: g is coretraction by A1;

g is retraction

for f being Morphism of o1,o2 holds f is coretraction ) implies for a, b being Object of C

for g being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds

g is iso )

assume A1: for o1, o2 being Object of C

for f being Morphism of o1,o2 holds f is coretraction ; :: thesis: for a, b being Object of C

for g being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds

g is iso

let a, b be Object of C; :: thesis: for g being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds

g is iso

let g be Morphism of a,b; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies g is iso )

assume that

A2: <^a,b^> <> {} and

A3: <^b,a^> <> {} ; :: thesis: g is iso

A4: g is coretraction by A1;

g is retraction

proof

hence
g is iso
by A2, A3, A4, ALTCAT_3:6; :: thesis: verum
consider f being Morphism of b,a such that

A5: f is_left_inverse_of g by A4;

take f ; :: according to ALTCAT_3:def 2 :: thesis: g is_left_inverse_of f

A6: f is mono by A1, A2, A3, ALTCAT_3:16;

f * (g * f) = (f * g) * f by A2, A3, ALTCAT_1:21

.= (idm a) * f by A5

.= f by A3, ALTCAT_1:20

.= f * (idm b) by A3, ALTCAT_1:def 17 ;

hence g * f = idm b by A6; :: according to ALTCAT_3:def 1 :: thesis: verum

end;A5: f is_left_inverse_of g by A4;

take f ; :: according to ALTCAT_3:def 2 :: thesis: g is_left_inverse_of f

A6: f is mono by A1, A2, A3, ALTCAT_3:16;

f * (g * f) = (f * g) * f by A2, A3, ALTCAT_1:21

.= (idm a) * f by A5

.= f by A3, ALTCAT_1:20

.= f * (idm b) by A3, ALTCAT_1:def 17 ;

hence g * f = idm b by A6; :: according to ALTCAT_3:def 1 :: thesis: verum