theorem Th25: :: ISOCAT_2:27

for A, B, C being Category
for G being Functor of A, Functors (B,C) ex F being Functor of [:A,B:],C st G = export F