theorem Th1: :: ISOCAT_1:3

for A, B being Category
for F being Functor of A,B
for a, b being Object of A
for f being Morphism of a,b st f is invertible holds
F /. f is invertible