let A, B, C be Category; :: thesis: Functors ([:A,B:],C) ~= Functors (A,(Functors (B,C)))
take export (A,B,C) ; :: according to ISOCAT_1:def 4 :: thesis: export (A,B,C) is isomorphic
thus export (A,B,C) is isomorphic ; :: thesis: verum