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