thus distribute (A,B,C) is one-to-one :: according to ISOCAT_1:def 3 :: thesis: rng (distribute (A,B,C)) = the carrier' of [:(Functors (A,B)),(Functors (A,C)):]

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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)) ; :: thesis: ( 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)) ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

thus rng (distribute (A,B,C)) c= the carrier' of [:(Functors (A,B)),(Functors (A,C)):] ; :: according to XBOOLE_0:def 10 :: thesis: the carrier' of [:(Functors (A,B)),(Functors (A,C)):] c= rng (distribute (A,B,C))
let o be object ; :: according to TARSKI:def 3 :: thesis: ( 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)):] ; :: thesis: 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; :: thesis: verum