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 ((pr1 A,B) * (pr1 [:A,B:],C)) = the carrier' of [:[:A,B:],C:]
by FUNCT_2:def 1;
A2:
dom <:((pr2 A,B) * (pr1 [:A,B:],C)),(pr2 [:A,B:],C):> = the carrier' of [:[:A,B:],C:]
by FUNCT_2:def 1;
A3:
dom (pr2 [:A,B:],C) = the carrier' of [:[:A,B:],C:]
by FUNCT_2:def 1;
A4:
dom ((pr2 A,B) * (pr1 [: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 A5:
(
x1 in [:the carrier' of A,the carrier' of B:] &
x2 in the
carrier' of
C )
and A6:
x = [x1,x2]
by ZFMISC_1:def 2;
consider x11,
x12 being
set such that A7:
(
x11 in the
carrier' of
A &
x12 in the
carrier' of
B )
and A8:
x1 = [x11,x12]
by A5, 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 A9:
(
y1 in [:the carrier' of A,the carrier' of B:] &
y2 in the
carrier' of
C )
and A10:
y = [y1,y2]
by ZFMISC_1:def 2;
consider y11,
y12 being
set such that A11:
(
y11 in the
carrier' of
A &
y12 in the
carrier' of
B )
and A12:
y1 = [y11,y12]
by A9, ZFMISC_1:def 2;
reconsider f11 =
x11,
g11 =
y11 as
Morphism of
A by A7, A11;
reconsider f12 =
x12,
g12 =
y12 as
Morphism of
B by A7, A11;
reconsider f2 =
x2,
g2 =
y2 as
Morphism of
C by A5, A9;
assume A13:
F . x = F . y
;
:: thesis: x = yA14:
[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 A3, A4, FUNCT_3:69
.=
F . [[g11,g12],g2]
by A1, A2, A6, A8, A10, A12, A13, 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 A1, 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 A3, A4, 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
(
x11 = y11 &
[x12,x2] = [y12,y2] )
by ZFMISC_1:33;
then
(
x12 = y12 &
x2 = y2 )
by ZFMISC_1:33;
hence
x = y
by A6, A8, A10, A12, A14, 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
A15:
( x1 in the carrier' of A & x2 in the carrier' of [:B,C:] )
and
A16:
x = [x1,x2]
by ZFMISC_1:def 2;
consider x21, x22 being set such that
A17:
( x21 in the carrier' of B & x22 in the carrier' of C )
and
A18:
x2 = [x21,x22]
by A15, ZFMISC_1:def 2;
reconsider x1 = x1 as Morphism of A by A15;
reconsider x21 = x21 as Morphism of B by A17;
reconsider x22 = x22 as Morphism of C by A17;
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 A1, 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 A3, A4, 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 A16, A18, FUNCT_2:6; :: thesis: verum