theorem Th22: :: ISOCAT_2:24

for A, B, C being Category
for F being Functor of [:A,B:],C holds id (export F) = export (id F)