theorem :: ISOCAT_2:29

for A, B, C being Category holds Functors ([:A,B:],C) ~= Functors (A,(Functors (B,C)))