theorem :: ISOCAT_2:40

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