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