let A, B, C be Category; [:[: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)):>:>; ISOCAT_1:def 4 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 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 = ylet x,
y be
object ;
( 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:]
;
( 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:]
;
( 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
;
x = yconsider 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;
verum end;
hence
F is one-to-one
by FUNCT_2:19; ISOCAT_1:def 3 rng F = the carrier' of [:A,[:B,C:]:]
thus
rng F c= the carrier' of [:A,[:B,C:]:]
; XBOOLE_0:def 10 the carrier' of [:A,[:B,C:]:] c= rng F
let x be object ; TARSKI:def 3 ( not x in the carrier' of [:A,[:B,C:]:] or x in rng F )
assume
x in the carrier' of [:A,[:B,C:]:]
; 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; verum