let A, B be category; :: thesis: ( A,B are_opposite implies for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso ) )
assume A1: A,B are_opposite ; :: thesis: for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso )
let a, b be Object of A; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso ) )
assume that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {} ; :: thesis: for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso )
let a9, b9 be Object of B; :: thesis: ( a9 = a & b9 = b implies for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso ) )
assume that
A4: a9 = a and
A5: b9 = b ; :: thesis: for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso )
A6: <^b9,a9^> = <^a,b^> by A1, A4, A5, Th9;
A7: <^a9,b9^> = <^b,a^> by A1, A4, A5, Th9;

now :: thesis: for A, B being category st A,B are_opposite holds
for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso

let A, B be category; :: thesis: ( A,B are_opposite implies for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso )
assume A8: A,B are_opposite ; :: thesis: for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso
let a, b be Object of A; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso )
assume that
A9: <^a,b^> <> {} and
A10: <^b,a^> <> {} ; :: thesis: for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso
let a9, b9 be Object of B; :: thesis: ( a9 = a & b9 = b implies for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso )
assume that
A11: a9 = a and
A12: b9 = b ; :: thesis: for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso
let f be Morphism of a,b; :: thesis: for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso
let f9 be Morphism of b9,a9; :: thesis: ( f9 = f & f is iso implies f9 is iso )
assume A13: f9 = f ; :: thesis: ( f is iso implies f9 is iso )
assume A14: f is iso ; :: thesis: f9 is iso
then A15: f * (f ") = idm b ;
A16: (f ") * f = idm a by A14;
( f is retraction & f is coretraction ) by A14, ALTCAT_3:5;
then A17: f9 " = f " by A8, A9, A10, A11, A12, A13, Th22;
A18: idm a = idm a9 by A8, A11, Th10;
A19: idm b = idm b9 by A8, A12, Th10;
A20: f9 * (f9 ") = idm a9 by A8, A9, A10, A11, A12, A13, A16, A17, A18, Th9;
(f9 ") * f9 = idm b9 by A8, A9, A10, A11, A12, A13, A15, A17, A19, Th9;
hence f9 is iso by A20; :: thesis: verum

end;

hence for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso ) by A1, A2, A3, A4, A5, A6, A7; :: thesis: verum