let A be Category; for o, m being set holds [:(1Cat (o,m)),A:] ~= A
let o, m be set ; [:(1Cat (o,m)),A:] ~= A
take F = pr2 ((1Cat (o,m)),A); ISOCAT_1:def 4 F is isomorphic
set X = [: the carrier' of (1Cat (o,m)), the carrier' of A:];
now for x1, x2 being object st x1 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] & x2 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] & F . x1 = F . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] & x2 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] & F . x1 = F . x2 implies x1 = x2 )assume
x1 in [: the carrier' of (1Cat (o,m)), the carrier' of A:]
;
( x2 in [: the carrier' of (1Cat (o,m)), the carrier' of A:] & F . x1 = F . x2 implies x1 = x2 )then consider x11,
x12 being
object such that A1:
x11 in the
carrier' of
(1Cat (o,m))
and A2:
x12 in the
carrier' of
A
and A3:
x1 = [x11,x12]
by ZFMISC_1:def 2;
assume
x2 in [: the carrier' of (1Cat (o,m)), the carrier' of A:]
;
( F . x1 = F . x2 implies x1 = x2 )then consider x21,
x22 being
object such that A4:
x21 in the
carrier' of
(1Cat (o,m))
and A5:
x22 in the
carrier' of
A
and A6:
x2 = [x21,x22]
by ZFMISC_1:def 2;
reconsider f11 =
x11,
f21 =
x21 as
Morphism of
(1Cat (o,m)) by A1, A4;
assume A7:
F . x1 = F . x2
;
x1 = x2reconsider f12 =
x12,
f22 =
x22 as
Morphism of
A by A2, A5;
A8:
f11 =
m
by TARSKI:def 1
.=
f21
by TARSKI:def 1
;
f12 =
F . (
f11,
f12)
by FUNCT_3:def 5
.=
F . (
f21,
f22)
by A3, A6, A7
.=
f22
by FUNCT_3:def 5
;
hence
x1 = x2
by A3, A6, A8;
verum end;
hence
F is one-to-one
by FUNCT_2:19; ISOCAT_1:def 3 rng F = the carrier' of A
thus
rng F = the carrier' of A
by FUNCT_3:46; verum