let A, B be category; :: thesis: for F being contravariant Functor of A,B
for o1, o2 being Object of A st o1,o2 are_iso holds
F . o2,F . o1 are_iso
let F be contravariant Functor of A,B; :: thesis: for o1, o2 being Object of A st o1,o2 are_iso holds
F . o2,F . o1 are_iso
let o1, o2 be Object of A; :: thesis: ( o1,o2 are_iso implies F . o2,F . o1 are_iso )
assume A1: o1,o2 are_iso ; :: thesis: F . o2,F . o1 are_iso
then consider a being Morphism of o1,o2 such that
A2: a is iso ;
A3: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A1;
hence ( <^(F . o2),(F . o1)^> <> {} & <^(F . o1),(F . o2)^> <> {} ) by FUNCTOR0:def 19; :: according to ALTCAT_3:def 6 :: thesis: ex b₁ being M3(<^(F . o2),(F . o1)^>) st b₁ is iso
take F . a ; :: thesis: F . a is iso
thus F . a is iso by A3, A2, Th24; :: thesis: verum