thus
export (A,B,C) is one-to-one
ISOCAT_1:def 3 rng (export (A,B,C)) = the carrier' of (Functors (A,(Functors (B,C))))proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( 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))
;
( 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))
;
( 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
;
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;
verum
end;
thus
rng (export (A,B,C)) c= the carrier' of (Functors (A,(Functors (B,C))))
; XBOOLE_0:def 10 the carrier' of (Functors (A,(Functors (B,C)))) c= rng (export (A,B,C))
let m be object ; TARSKI:def 3 ( 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))))
; 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; verum