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