let A be Category; :: thesis: for o, m being set holds [:(1Cat (o,m)),A:] ~= A
let o, m be set ; :: thesis: [:(1Cat (o,m)),A:] ~= A
take F = pr2 ((1Cat (o,m)),A); :: according to ISOCAT_1:def 4 :: thesis: F is isomorphic
set X = [: the carrier' of (1Cat (o,m)), the carrier' of A:];

now :: thesis: 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 = x2

let x1, x2 be object ; :: thesis: ( 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:] ; :: thesis: ( 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:] ; :: thesis: ( 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 ; :: thesis: x1 = x2
reconsider 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; :: 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
thus rng F = the carrier' of A by FUNCT_3:46; :: thesis: verum