let C be category; 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; 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; ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso implies m " is iso )
assume A1:
( <^o1,o2^> <> {} & <^o2,o1^> <> {} )
; ( not m is iso or m " is iso )
assume
m is iso
; 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
;
ALTCAT_3:def 5 ((m ") ") * (m ") = idm o2
thus ((m ") ") * (m ") =
m * (m ")
by A1, A2, ALTCAT_3:3
.=
idm o2
by A1, A2, ALTCAT_3:2
; verum