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:33;
p in the Arrows of (AllIso C) . (o1,o2) by A1;
then A2: ( <^p1,p2^> <> {} & <^p2,p1^> <> {} ) by Def5;
A3: p is iso by A1, Def5;
then A4: p " is iso by A2, Th3;
then A5: p " in the Arrows of (AllIso C) . (p2,p1) by A2, Def5;
reconsider m1 = p " as Morphism of o2,o1 by A2, A4, 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, A5, ALTCAT_2:32
.= idm p2 by A3
.= idm o2 by ALTCAT_2:34 ; :: according to ALTCAT_3:def 1 :: thesis: verum
end;
A7: 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, A5, ALTCAT_2:32
.= idm p1 by A3
.= idm o1 by ALTCAT_2:34 ; :: according to ALTCAT_3:def 1 :: thesis: verum
end;
p " in <^o2,o1^> by A2, A4, Def5;
hence m is iso by A1, A6, A7, ALTCAT_3:6; :: thesis: m " in <^o2,o1^>
thus m " in <^o2,o1^> by A5; :: thesis: verum