thus
distribute (A,B,C) is one-to-one
ISOCAT_1:def 3 rng (distribute (A,B,C)) = the carrier' of [:(Functors (A,B)),(Functors (A,C)):]proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom (distribute (A,B,C)) or not x2 in dom (distribute (A,B,C)) or not (distribute (A,B,C)) . x1 = (distribute (A,B,C)) . x2 or x1 = x2 )
assume
x1 in dom (distribute (A,B,C))
;
( not x2 in dom (distribute (A,B,C)) or not (distribute (A,B,C)) . x1 = (distribute (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:],
s 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],s]
by Th6;
assume
x2 in dom (distribute (A,B,C))
;
( not (distribute (A,B,C)) . x1 = (distribute (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:],
t 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],t]
by Th6;
assume
(distribute (A,B,C)) . x1 = (distribute (A,B,C)) . x2
;
x1 = x2
then A5:
[[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]] =
(distribute (A,B,C)) . [[G1,G2],t]
by A1, A2, A4, Def13
.=
[[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]]
by A3, Def13
;
then A6:
[[(Pr1 F1),(Pr1 F2)],(Pr1 s)] = [[(Pr1 G1),(Pr1 G2)],(Pr1 t)]
by XTUPLE_0:1;
A7:
[[(Pr2 F1),(Pr2 F2)],(Pr2 s)] = [[(Pr2 G1),(Pr2 G2)],(Pr2 t)]
by A5, XTUPLE_0:1;
then A8:
Pr2 s = Pr2 t
by XTUPLE_0:1;
A9:
[(Pr2 F1),(Pr2 F2)] = [(Pr2 G1),(Pr2 G2)]
by A7, XTUPLE_0:1;
then A10:
Pr2 F1 = Pr2 G1
by XTUPLE_0:1;
A11:
[(Pr1 F1),(Pr1 F2)] = [(Pr1 G1),(Pr1 G2)]
by A6, XTUPLE_0:1;
then
Pr1 F1 = Pr1 G1
by XTUPLE_0:1;
then A12:
F1 = G1
by A10, Th30;
Pr1 s = Pr1 t
by A6, XTUPLE_0:1;
then A13:
s = t
by A1, A3, A8, Th31;
A14:
Pr2 F2 = Pr2 G2
by A9, XTUPLE_0:1;
Pr1 F2 = Pr1 G2
by A11, XTUPLE_0:1;
hence
x1 = x2
by A2, A4, A14, A13, A12, Th30;
verum
end;
thus
rng (distribute (A,B,C)) c= the carrier' of [:(Functors (A,B)),(Functors (A,C)):]
; XBOOLE_0:def 10 the carrier' of [:(Functors (A,B)),(Functors (A,C)):] c= rng (distribute (A,B,C))
let o be object ; TARSKI:def 3 ( not o in the carrier' of [:(Functors (A,B)),(Functors (A,C)):] or o in rng (distribute (A,B,C)) )
assume
o in the carrier' of [:(Functors (A,B)),(Functors (A,C)):]
; o in rng (distribute (A,B,C))
then consider o1 being Morphism of (Functors (A,B)), o2 being Morphism of (Functors (A,C)) such that
A15:
o = [o1,o2]
by CAT_2:27;
consider G1, G2 being Functor of A,C, t being natural_transformation of G1,G2 such that
A16:
G1 is_naturally_transformable_to G2
and
dom o2 = G1
and
cod o2 = G2
and
A17:
o2 = [[G1,G2],t]
by Th6;
consider F1, F2 being Functor of A,B, s being natural_transformation of F1,F2 such that
A18:
F1 is_naturally_transformable_to F2
and
dom o1 = F1
and
cod o1 = F2
and
A19:
o1 = [[F1,F2],s]
by Th6;
set f = [[<:F1,G1:>,<:F2,G2:>],<:s,t:>];
A20:
<:F1,G1:> is_naturally_transformable_to <:F2,G2:>
by A18, A16, Th36;
then
[[<:F1,G1:>,<:F2,G2:>],<:s,t:>] in NatTrans (A,[:B,C:])
by NATTRA_1:32;
then reconsider f = [[<:F1,G1:>,<:F2,G2:>],<:s,t:>] as Morphism of (Functors (A,[:B,C:])) by NATTRA_1:def 17;
A21:
( Pr1 <:F1,G1:> = F1 & Pr1 <:F2,G2:> = F2 )
by Th29;
A22:
( Pr2 <:F1,G1:> = G1 & Pr2 <:F2,G2:> = G2 )
by Th29;
( Pr1 <:s,t:> = s & Pr2 <:s,t:> = t )
by A18, A16, Th37;
then
(distribute (A,B,C)) . f = o
by A15, A19, A17, A20, A21, A22, Def13;
hence
o in rng (distribute (A,B,C))
by FUNCT_2:112; verum