let A, B be Category; :: thesis: [:A,B:] ~= [:B,A:]
take F = <:(pr2 (A,B)),(pr1 (A,B)):>; :: according to ISOCAT_1:def 4 :: thesis: F is isomorphic
A1: ( dom (pr1 (A,B)) = the carrier' of [:A,B:] & dom (pr2 (A,B)) = the carrier' of [:A,B:] ) by FUNCT_2:def 1;

now :: thesis: for x1, x2 being object st x1 in [: the carrier' of A, the carrier' of B:] & x2 in [: the carrier' of A, the carrier' of B:] & F . x1 = F . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in [: the carrier' of A, the carrier' of B:] & x2 in [: the carrier' of A, the carrier' of B:] & F . x1 = F . x2 implies x1 = x2 )
assume x1 in [: the carrier' of A, the carrier' of B:] ; :: thesis: ( x2 in [: the carrier' of A, the carrier' of B:] & F . x1 = F . x2 implies x1 = x2 )
then consider x11, x12 being object such that
A2: x11 in the carrier' of A and
A3: x12 in the carrier' of B and
A4: x1 = [x11,x12] by ZFMISC_1:def 2;
assume x2 in [: the carrier' of A, the carrier' of B:] ; :: thesis: ( F . x1 = F . x2 implies x1 = x2 )
then consider x21, x22 being object such that
A5: x21 in the carrier' of A and
A6: x22 in the carrier' of B and
A7: x2 = [x21,x22] by ZFMISC_1:def 2;
reconsider f12 = x12, f22 = x22 as Morphism of B by A3, A6;
reconsider f11 = x11, f21 = x21 as Morphism of A by A2, A5;
A8: [f21,f22] in the carrier' of [:A,B:] ;
assume A9: F . x1 = F . x2 ; :: thesis: x1 = x2
A10: [f11,f12] in the carrier' of [:A,B:] ;
A11: [f12,f11] = [f12,((pr1 (A,B)) . (f11,f12))] by FUNCT_3:def 4
.= [((pr2 (A,B)) . (f11,f12)),((pr1 (A,B)) . (f11,f12))] by FUNCT_3:def 5
.= F . (f21,f22) by A1, A4, A7, A10, A9, FUNCT_3:49
.= [((pr2 (A,B)) . (f21,f22)),((pr1 (A,B)) . (f21,f22))] by A1, A8, FUNCT_3:49
.= [f22,((pr1 (A,B)) . (f21,f22))] by FUNCT_3:def 5
.= [f22,f21] by FUNCT_3:def 4 ;
then x12 = x22 by XTUPLE_0:1;
hence x1 = x2 by A4, A7, A11, XTUPLE_0:1; :: 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 [:B,A:]
thus rng F c= the carrier' of [:B,A:] ; :: according to XBOOLE_0:def 10 :: thesis: the carrier' of [:B,A:] c= rng F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier' of [:B,A:] or x in rng F )
assume x in the carrier' of [:B,A:] ; :: thesis: x in rng F
then consider x1, x2 being object such that
A12: x1 in the carrier' of B and
A13: x2 in the carrier' of A and
A14: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x2 = x2 as Morphism of A by A13;
reconsider x1 = x1 as Morphism of B by A12;
F . [x2,x1] = [((pr2 (A,B)) . (x2,x1)),((pr1 (A,B)) . (x2,x1))] by A1, FUNCT_3:49
.= [x1,((pr1 (A,B)) . (x2,x1))] by FUNCT_3:def 5
.= [x1,x2] by FUNCT_3:def 4 ;
hence x in rng F by A14, FUNCT_2:4; :: thesis: verum