let A, B, C be Category; :: thesis: [:[:A,B:],C:] ~= [:A,[:B,C:]:]
set X = (pr1 (A,B)) * (pr1 ([:A,B:],C));
set Y = <:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):>;
take F = <:((pr1 (A,B)) * (pr1 ([:A,B:],C))),<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):>:>; :: according to ISOCAT_1:def 4 :: thesis: F is isomorphic
A1: ( dom (pr2 ([:A,B:],C)) = the carrier' of [:[:A,B:],C:] & dom ((pr2 (A,B)) * (pr1 ([:A,B:],C))) = the carrier' of [:[:A,B:],C:] ) by FUNCT_2:def 1;
A2: ( dom ((pr1 (A,B)) * (pr1 ([:A,B:],C))) = the carrier' of [:[:A,B:],C:] & dom <:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> = the carrier' of [:[:A,B:],C:] ) by FUNCT_2:def 1;

now :: thesis: for x, y being object st x in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] & y in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] & F . x = F . y holds
x = y

let x, y be object ; :: thesis: ( x in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] & y in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] & F . x = F . y implies x = y )
assume x in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] ; :: thesis: ( y in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] & F . x = F . y implies x = y )
then consider x1, x2 being object such that
A3: x1 in [: the carrier' of A, the carrier' of B:] and
A4: x2 in the carrier' of C and
A5: x = [x1,x2] by ZFMISC_1:def 2;
assume y in [:[: the carrier' of A, the carrier' of B:], the carrier' of C:] ; :: thesis: ( F . x = F . y implies x = y )
then consider y1, y2 being object such that
A6: y1 in [: the carrier' of A, the carrier' of B:] and
A7: y2 in the carrier' of C and
A8: y = [y1,y2] by ZFMISC_1:def 2;
reconsider f2 = x2, g2 = y2 as Morphism of C by A4, A7;
assume A9: F . x = F . y ; :: thesis: x = y
consider x11, x12 being object such that
A10: x11 in the carrier' of A and
A11: x12 in the carrier' of B and
A12: x1 = [x11,x12] by A3, ZFMISC_1:def 2;
consider y11, y12 being object such that
A13: y11 in the carrier' of A and
A14: y12 in the carrier' of B and
A15: y1 = [y11,y12] by A6, ZFMISC_1:def 2;
reconsider f12 = x12, g12 = y12 as Morphism of B by A11, A14;
reconsider f11 = x11, g11 = y11 as Morphism of A by A10, A13;
A16: [f11,[f12,f2]] = [((pr1 (A,B)) . (f11,f12)),[f12,f2]] by FUNCT_3:def 4
.= [((pr1 (A,B)) . ((pr1 ([:A,B:],C)) . ([f11,f12],f2))),[f12,f2]] by FUNCT_3:def 4
.= [((pr1 (A,B)) . ((pr1 ([:A,B:],C)) . [[f11,f12],f2])),[f12,f2]]
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . ([f11,f12],f2)),[f12,f2]] by FUNCT_2:15
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),[((pr2 (A,B)) . (f11,f12)),f2]] by FUNCT_3:def 5
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),[((pr2 (A,B)) . ((pr1 ([:A,B:],C)) . ([f11,f12],f2))),f2]] by FUNCT_3:def 4
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),f2]] by FUNCT_2:15
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),((pr2 ([:A,B:],C)) . ([f11,f12],f2))]] by FUNCT_3:def 5
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[f11,f12],f2]),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[f11,f12],f2])] by A1, FUNCT_3:49
.= F . [[g11,g12],g2] by A2, A5, A12, A8, A15, A9, FUNCT_3:49
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[g11,g12],g2])] by A2, FUNCT_3:49
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),((pr2 ([:A,B:],C)) . ([g11,g12],g2))]] by A1, FUNCT_3:49
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),g2]] by FUNCT_3:def 5
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[((pr2 (A,B)) . ((pr1 ([:A,B:],C)) . ([g11,g12],g2))),g2]] by FUNCT_2:15
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[((pr2 (A,B)) . (g11,g12)),g2]] by FUNCT_3:def 4
.= [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[g11,g12],g2]),[g12,g2]] by FUNCT_3:def 5
.= [((pr1 (A,B)) . ((pr1 ([:A,B:],C)) . ([g11,g12],g2))),[g12,g2]] by FUNCT_2:15
.= [((pr1 (A,B)) . (g11,g12)),[g12,g2]] by FUNCT_3:def 4
.= [g11,[g12,g2]] by FUNCT_3:def 4 ;
then [x12,x2] = [y12,y2] by XTUPLE_0:1;
then ( x12 = y12 & x2 = y2 ) by XTUPLE_0:1;
hence x = y by A5, A12, A8, A15, A16, XTUPLE_0:1; :: thesis: verum

end;

hence F is one-to-one by FUNCT_2:19; :: according to ISOCAT_1:def 3 :: thesis: rng F = the carrier' of [:A,[:B,C:]:]
thus rng F c= the carrier' of [:A,[:B,C:]:] ; :: according to XBOOLE_0:def 10 :: thesis: the carrier' of [:A,[:B,C:]:] c= rng F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier' of [:A,[:B,C:]:] or x in rng F )
assume x in the carrier' of [:A,[:B,C:]:] ; :: thesis: x in rng F
then consider x1, x2 being object such that
A17: x1 in the carrier' of A and
A18: x2 in the carrier' of [:B,C:] and
A19: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 = x1 as Morphism of A by A17;
consider x21, x22 being object such that
A20: x21 in the carrier' of B and
A21: x22 in the carrier' of C and
A22: x2 = [x21,x22] by A18, ZFMISC_1:def 2;
reconsider x22 = x22 as Morphism of C by A21;
reconsider x21 = x21 as Morphism of B by A20;
F . [[x1,x21],x22] = [(((pr1 (A,B)) * (pr1 ([:A,B:],C))) . [[x1,x21],x22]),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[x1,x21],x22])] by A2, FUNCT_3:49
.= [((pr1 (A,B)) . ((pr1 ([:A,B:],C)) . ([x1,x21],x22))),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[x1,x21],x22])] by FUNCT_2:15
.= [((pr1 (A,B)) . (x1,x21)),(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[x1,x21],x22])] by FUNCT_3:def 4
.= [x1,(<:((pr2 (A,B)) * (pr1 ([:A,B:],C))),(pr2 ([:A,B:],C)):> . [[x1,x21],x22])] by FUNCT_3:def 4
.= [x1,[(((pr2 (A,B)) * (pr1 ([:A,B:],C))) . [[x1,x21],x22]),((pr2 ([:A,B:],C)) . [[x1,x21],x22])]] by A1, FUNCT_3:49
.= [x1,[((pr2 (A,B)) . ((pr1 ([:A,B:],C)) . ([x1,x21],x22))),((pr2 ([:A,B:],C)) . [[x1,x21],x22])]] by FUNCT_2:15
.= [x1,[((pr2 (A,B)) . (x1,x21)),((pr2 ([:A,B:],C)) . ([x1,x21],x22))]] by FUNCT_3:def 4
.= [x1,[x21,((pr2 ([:A,B:],C)) . ([x1,x21],x22))]] by FUNCT_3:def 5
.= [x1,[x21,x22]] by FUNCT_3:def 5 ;
hence x in rng F by A19, A22, FUNCT_2:4; :: thesis: verum