for A, B being category
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