let A, B, C be Category; :: thesis: export A,B,C is isomorphic
A1: dom (export A,B,C) = the carrier' of (Functors [:A,B:],C) by FUNCT_2:def 1;
thus export A,B,C is one-to-one :: according to ISOCAT_1:def 3 :: thesis: rng (export A,B,C) = the carrier' of (Functors A,(Functors B,C))

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 (export A,B,C) or not x2 in proj1 (export A,B,C) or not (export A,B,C) . x1 = (export A,B,C) . x2 or x1 = x2 )
assume x1 in dom (export A,B,C) ; :: thesis: ( not x2 in proj1 (export A,B,C) or not (export A,B,C) . x1 = (export A,B,C) . x2 or x1 = x2 )
then reconsider f1 = x1 as Morphism of (Functors [:A,B:],C) ;
consider F1, F2 being Functor of [:A,B:],C, t being natural_transformation of F1,F2 such that
A2: F1 is_naturally_transformable_to F2 and
A3: ( dom f1 = F1 & cod f1 = F2 & f1 = [[F1,F2],t] ) by Th9;
assume x2 in dom (export A,B,C) ; :: thesis: ( not (export A,B,C) . x1 = (export A,B,C) . x2 or x1 = x2 )
then reconsider f2 = x2 as Morphism of (Functors [:A,B:],C) ;
consider G1, G2 being Functor of [:A,B:],C, u being natural_transformation of G1,G2 such that
A4: G1 is_naturally_transformable_to G2 and
A5: ( dom f2 = G1 & cod f2 = G2 & f2 = [[G1,G2],u] ) by Th9;
assume (export A,B,C) . x1 = (export A,B,C) . x2 ; :: thesis: x1 = x2
then [[(export F1),(export F2)],(export t)] = (export A,B,C) . [[G1,G2],u] by A2, A3, A5, Def6
.= [[(export G1),(export G2)],(export u)] by A4, Def6 ;
then A6: ( [(export F1),(export F2)] = [(export G1),(export G2)] & export u = export t ) by ZFMISC_1:33;
then ( export F1 = export G1 & export F2 = export G2 ) by ZFMISC_1:33;
then ( F1 = G1 & F2 = G2 ) by Th26;
hence x1 = x2 by A2, A3, A5, A6, Th30; :: thesis: verum

end;

thus rng (export A,B,C) c= the carrier' of (Functors A,(Functors B,C)) ; :: according to XBOOLE_0:def 10 :: thesis: the carrier' of (Functors A,(Functors B,C)) c= rng (export A,B,C)
let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in the carrier' of (Functors A,(Functors B,C)) or m in rng (export A,B,C) )
assume m in the carrier' of (Functors A,(Functors B,C)) ; :: thesis: m in rng (export A,B,C)
then reconsider f = m as Morphism of (Functors A,(Functors B,C)) ;
consider F1, F2 being Functor of A, Functors B,C, t being natural_transformation of F1,F2 such that
A7: F1 is_naturally_transformable_to F2 and
A8: ( dom f = F1 & cod f = F2 & f = [[F1,F2],t] ) by Th9;
consider G1 being Functor of [:A,B:],C such that
A9: F1 = export G1 by Th31;
consider G2 being Functor of [:A,B:],C such that
A10: F2 = export G2 by Th31;
A11: G1 is_naturally_transformable_to G2 by A7, A9, A10, Th32;
consider u being natural_transformation of G1,G2 such that
A12: t = export u by A7, A9, A10, Th32;
A13: (export A,B,C) . [[G1,G2],u] = f by A8, A9, A10, A11, A12, Def6;
[[G1,G2],u] in NatTrans [:A,B:],C by A11, NATTRA_1:35;
then [[G1,G2],u] in dom (export A,B,C) by A1, NATTRA_1:def 18;
hence m in rng (export A,B,C) by A13, FUNCT_1:def 5; :: thesis: verum