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

let x1, x2 be set ; :: 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 set 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 set 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 5
.= [((pr2 A,B) . f11,f12),((pr1 A,B) . f11,f12)] by FUNCT_3:def 6
.= F . f21,f22 by A1, A4, A7, A10, A9, FUNCT_3:69
.= [((pr2 A,B) . f21,f22),((pr1 A,B) . f21,f22)] by A1, A8, FUNCT_3:69
.= [f22,((pr1 A,B) . f21,f22)] by FUNCT_3:def 6
.= [f22,f21] by FUNCT_3:def 5 ;
then x12 = x22 by ZFMISC_1:33;
hence x1 = x2 by A4, A7, A11, ZFMISC_1:33; :: 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 [: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 set ; :: 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 set 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:69
.= [x1,((pr1 A,B) . x2,x1)] by FUNCT_3:def 6
.= [x1,x2] by FUNCT_3:def 5 ;
hence x in rng F by A14, FUNCT_2:6; :: thesis: verum