let C be category; :: thesis: for o1, o2 being Object of C
for m being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso holds
m " is iso
let o1, o2 be Object of C; :: thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso holds
m " is iso
let m be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso implies m " is iso )
assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; :: thesis: ( not m is iso or m " is iso )
assume m is iso ; :: thesis: m " is iso
then A2: ( m is retraction & m is coretraction ) by ALTCAT_3:5;
hence (m ") * ((m ") ") = (m ") * m by A1, ALTCAT_3:3
.= idm o1 by A1, A2, ALTCAT_3:2 ;
:: according to ALTCAT_3:def 5 :: thesis: ((m ") ") * (m ") = idm o2
thus ((m ") ") * (m ") = m * (m ") by A1, A2, ALTCAT_3:3
.= idm o2 by A1, A2, ALTCAT_3:2 ; :: thesis: verum