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 object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (export (A,B,C)) or not x2 in dom (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 dom (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
A1: F1 is_naturally_transformable_to F2 and
dom f1 = F1 and
cod f1 = F2 and
A2: f1 = [[F1,F2],t] by Th6;
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
A3: G1 is_naturally_transformable_to G2 and
dom f2 = G1 and
cod f2 = G2 and
A4: f2 = [[G1,G2],u] by Th6;
assume (export (A,B,C)) . x1 = (export (A,B,C)) . x2 ; :: thesis: x1 = x2
then A5: [[(export F1),(export F2)],(export t)] = (export (A,B,C)) . [[G1,G2],u] by A1, A2, A4, Def6
.= [[(export G1),(export G2)],(export u)] by A3, Def6 ;
then A6: [(export F1),(export F2)] = [(export G1),(export G2)] by XTUPLE_0:1;
then export F1 = export G1 by XTUPLE_0:1;
then A7: F1 = G1 by Th20;
export F2 = export G2 by A6, XTUPLE_0:1;
then A8: F2 = G2 by Th20;
export u = export t by A5, XTUPLE_0:1;
hence x1 = x2 by A1, A2, A4, A7, A8, Th24; :: 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 object ; :: 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
A9: F1 is_naturally_transformable_to F2 and
dom f = F1 and
cod f = F2 and
A10: f = [[F1,F2],t] by Th6;
consider G1 being Functor of [:A,B:],C such that
A11: F1 = export G1 by Th25;
consider G2 being Functor of [:A,B:],C such that
A12: F2 = export G2 by Th25;
consider u being natural_transformation of G1,G2 such that
A13: t = export u by A9, A11, A12, Th26;
A14: G1 is_naturally_transformable_to G2 by A9, A11, A12, Th26;
then ( dom (export (A,B,C)) = the carrier' of (Functors ([:A,B:],C)) & [[G1,G2],u] in NatTrans ([:A,B:],C) ) by FUNCT_2:def 1, NATTRA_1:32;
then A15: [[G1,G2],u] in dom (export (A,B,C)) by NATTRA_1:def 17;
(export (A,B,C)) . [[G1,G2],u] = f by A10, A11, A12, A14, A13, Def6;
hence m in rng (export (A,B,C)) by A15, FUNCT_1:def 3; :: thesis: verum