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 by Th48; :: thesis: verum