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

let x, y be set ; :: 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 set 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 set 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 set 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 set 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 5
.= [((pr1 A,B) . ((pr1 [:A,B:],C) . [f11,f12],f2)),[f12,f2]] by FUNCT_3:def 5
.= [((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:21
.= [(((pr1 A,B) * (pr1 [:A,B:],C)) . [[f11,f12],f2]),[((pr2 A,B) . f11,f12),f2]] by FUNCT_3:def 6
.= [(((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 5
.= [(((pr1 A,B) * (pr1 [:A,B:],C)) . [[f11,f12],f2]),[(((pr2 A,B) * (pr1 [:A,B:],C)) . [[f11,f12],f2]),f2]] by FUNCT_2:21
.= [(((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 6
.= [(((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:69
.= F . [[g11,g12],g2] by A2, A5, A12, A8, A15, A9, FUNCT_3:69
.= [(((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:69
.= [(((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:69
.= [(((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 6
.= [(((pr1 A,B) * (pr1 [:A,B:],C)) . [[g11,g12],g2]),[((pr2 A,B) . ((pr1 [:A,B:],C) . [g11,g12],g2)),g2]] by FUNCT_2:21
.= [(((pr1 A,B) * (pr1 [:A,B:],C)) . [[g11,g12],g2]),[((pr2 A,B) . g11,g12),g2]] by FUNCT_3:def 5
.= [(((pr1 A,B) * (pr1 [:A,B:],C)) . [[g11,g12],g2]),[g12,g2]] by FUNCT_3:def 6
.= [((pr1 A,B) . ((pr1 [:A,B:],C) . [g11,g12],g2)),[g12,g2]] by FUNCT_2:21
.= [((pr1 A,B) . g11,g12),[g12,g2]] by FUNCT_3:def 5
.= [g11,[g12,g2]] by FUNCT_3:def 5 ;
then [x12,x2] = [y12,y2] by ZFMISC_1:33;
then ( x12 = y12 & x2 = y2 ) by ZFMISC_1:33;
hence x = y by A5, A12, A8, A15, A16, ZFMISC_1:33; :: thesis: verum

end;

hence F is one-to-one by FUNCT_2:25; :: 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 set ; :: 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 set 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 set 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:69
.= [((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:21
.= [((pr1 A,B) . x1,x21),(<:((pr2 A,B) * (pr1 [:A,B:],C)),(pr2 [:A,B:],C):> . [[x1,x21],x22])] by FUNCT_3:def 5
.= [x1,(<:((pr2 A,B) * (pr1 [:A,B:],C)),(pr2 [:A,B:],C):> . [[x1,x21],x22])] by FUNCT_3:def 5
.= [x1,[(((pr2 A,B) * (pr1 [:A,B:],C)) . [[x1,x21],x22]),((pr2 [:A,B:],C) . [[x1,x21],x22])]] by A1, FUNCT_3:69
.= [x1,[((pr2 A,B) . ((pr1 [:A,B:],C) . [x1,x21],x22)),((pr2 [:A,B:],C) . [[x1,x21],x22])]] by FUNCT_2:21
.= [x1,[((pr2 A,B) . x1,x21),((pr2 [:A,B:],C) . [x1,x21],x22)]] by FUNCT_3:def 5
.= [x1,[x21,((pr2 [:A,B:],C) . [x1,x21],x22)]] by FUNCT_3:def 6
.= [x1,[x21,x22]] by FUNCT_3:def 6 ;
hence x in rng F by A19, A22, FUNCT_2:6; :: thesis: verum