let A, B be category; :: thesis: for F being contravariant Functor of A,B
for o1, o2 being object of A
for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is iso holds
F . a is iso
let F be contravariant Functor of A,B; :: thesis: for o1, o2 being object of A
for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is iso holds
F . a is iso
let o1, o2 be object of A; :: thesis: for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is iso holds
F . a is iso
let a be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is iso implies F . a is iso )
assume that
A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) and
A2: a is iso ; :: thesis: F . a is iso
A3: ( <^(F . o1),(F . o2)^> <> {} & <^(F . o2),(F . o1)^> <> {} ) by A1, FUNCTOR0:def 20;
( a is retraction & a is coretraction ) by A1, A2, ALTCAT_3:6;
then ( F . a is retraction & F . a is coretraction ) by A1, Th22, Th23;
hence F . a is iso by A3, ALTCAT_3:6; :: thesis: verum