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 a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is iso iff f' is iso ) )
assume A1: A,B are_opposite ; :: thesis: for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is iso iff f' is iso )
let a, b be object of A; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is iso iff f' is iso ) )
assume A2: ( <^a,b^> <> {} & <^b,a^> <> {} ) ; :: thesis: for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is iso iff f' is iso )
let a', b' be object of B; :: thesis: ( a' = a & b' = b implies for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is iso iff f' is iso ) )
assume A3: ( a' = a & b' = b ) ; :: thesis: for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is iso iff f' is iso )
A4: ( <^b',a'^> = <^a,b^> & <^a',b'^> = <^b,a^> ) by A1, A3, Th9;

now

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 a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f & f is iso holds
f' is iso )
assume A5: A,B are_opposite ; :: thesis: for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f & f is iso holds
f' is iso
let a, b be object of A; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f & f is iso holds
f' is iso )
assume A6: ( <^a,b^> <> {} & <^b,a^> <> {} ) ; :: thesis: for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f & f is iso holds
f' is iso
let a', b' be object of B; :: thesis: ( a' = a & b' = b implies for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f & f is iso holds
f' is iso )
assume A7: ( a' = a & b' = b ) ; :: thesis: for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f & f is iso holds
f' is iso
let f be Morphism of a,b; :: thesis: for f' being Morphism of b',a' st f' = f & f is iso holds
f' is iso
let f' be Morphism of b',a'; :: thesis: ( f' = f & f is iso implies f' is iso )
assume A8: f' = f ; :: thesis: ( f is iso implies f' is iso )
assume f is iso ; :: thesis: f' is iso
then A9: ( f * (f " ) = idm b & (f " ) * f = idm a & f is retraction & f is coretraction ) by ALTCAT_3:5, ALTCAT_3:def 5;
then ( f' " = f " & idm a = idm a' & idm b = idm b' ) by A5, A6, A7, A8, Th10, Th23;
then ( f' * (f' " ) = idm a' & (f' " ) * f' = idm b' ) by A5, A6, A7, A8, A9, Th9;
hence f' is iso by ALTCAT_3:def 5; :: thesis: verum

end;

hence for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is iso iff f' is iso ) by A1, A2, A3, A4; :: thesis: verum