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

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