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

let x1, x2 be set ; :: 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 set 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 set 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 6
.= F . f21,f22 by A3, A6, A7
.= f22 by FUNCT_3:def 6 ;
hence x1 = x2 by A3, A6, A8; :: 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
thus rng F = the carrier' of A by FUNCT_3:62; :: thesis: verum