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) & x12 in the carrier' of A ) and
A2: 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
A3: ( x21 in the carrier' of (1Cat o,m) & x22 in the carrier' of A ) and
A4: x2 = [x21,x22] by ZFMISC_1:def 2;
reconsider f11 = x11, f21 = x21 as Morphism of (1Cat o,m) by A1, A3;
reconsider f12 = x12, f22 = x22 as Morphism of A by A1, A3;
assume A5: F . x1 = F . x2 ; :: thesis: x1 = x2
A6: f12 = F . f11,f12 by FUNCT_3:def 6
.= F . f21,f22 by A2, A4, A5
.= f22 by FUNCT_3:def 6 ;
f11 = m by TARSKI:def 1
.= f21 by TARSKI:def 1 ;
hence x1 = x2 by A2, A4, A6; :: 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