let C be category; :: thesis: for o1, o2 being object of (AllIso C)
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
( m is iso & m " in <^o2,o1^> )
let o1, o2 be object of (AllIso C); :: thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
( m is iso & m " in <^o2,o1^> )
let m be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} implies ( m is iso & m " in <^o2,o1^> ) )
assume A1: <^o1,o2^> <> {} ; :: thesis: ( m is iso & m " in <^o2,o1^> )
reconsider p1 = o1, p2 = o2 as object of C by Def5;
reconsider p = m as Morphism of p1,p2 by A1, ALTCAT_2:34;
p in the Arrows of (AllIso C) . o1,o2 by A1;
then A2: ( <^p1,p2^> <> {} & <^p2,p1^> <> {} & p is iso ) by Def5;
then A3: p " is iso by Th3;
then A4: p " in the Arrows of (AllIso C) . p2,p1 by A2, Def5;
A5: p " in <^o2,o1^> by A2, A3, Def5;
reconsider m1 = p " as Morphism of o2,o1 by A2, A3, Def5;
A6: m is retraction

proof

take m1 ; :: according to ALTCAT_3:def 2 :: thesis: m is_left_inverse_of m1
thus m * m1 = p * (p " ) by A1, A4, ALTCAT_2:33
.= idm p2 by A2, ALTCAT_3:def 5
.= idm o2 by ALTCAT_2:35 ; :: according to ALTCAT_3:def 1 :: thesis: verum

end;

m is coretraction

proof

take m1 ; :: according to ALTCAT_3:def 3 :: thesis: m1 is_left_inverse_of m
thus m1 * m = (p " ) * p by A1, A4, ALTCAT_2:33
.= idm p1 by A2, ALTCAT_3:def 5
.= idm o1 by ALTCAT_2:35 ; :: according to ALTCAT_3:def 1 :: thesis: verum

end;

hence m is iso by A1, A5, A6, ALTCAT_3:6; :: thesis: m " in <^o2,o1^>
thus m " in <^o2,o1^> by A4; :: thesis: verum