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 & x12 in the carrier' of B ) and
A3: 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
A4: ( x21 in the carrier' of A & x22 in the carrier' of B ) and
A5: x2 = [x21,x22] by ZFMISC_1:def 2;
reconsider f11 = x11, f21 = x21 as Morphism of A by A2, A4;
reconsider f12 = x12, f22 = x22 as Morphism of B by A2, A4;
A6: [f21,f22] in the carrier' of [:A,B:] ;
A7: [f11,f12] in the carrier' of [:A,B:] ;
assume A8: F . x1 = F . x2 ; :: thesis: x1 = x2
[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, A3, A5, A7, A8, FUNCT_3:69
.= [((pr2 A,B) . f21,f22),((pr1 A,B) . f21,f22)] by A1, A6, FUNCT_3:69
.= [f22,((pr1 A,B) . f21,f22)] by FUNCT_3:def 6
.= [f22,f21] by FUNCT_3:def 5 ;
then ( x12 = x22 & x11 = x21 ) by ZFMISC_1:33;
hence x1 = x2 by A3, A5; :: 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
A9: ( x1 in the carrier' of B & x2 in the carrier' of A ) and
A10: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 = x1 as Morphism of B by A9;
reconsider x2 = x2 as Morphism of A by A9;
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 A10, FUNCT_2:6; :: thesis: verum