let X, Y be set ; :: thesis: <:(pr2 (X,Y)),(pr1 (X,Y)):> " = <:(pr2 (Y,X)),(pr1 (Y,X)):>
set f = <:(pr2 (X,Y)),(pr1 (X,Y)):>;
set g = <:(pr2 (Y,X)),(pr1 (Y,X)):>;
A1: dom (<:(pr2 (X,Y)),(pr1 (X,Y)):> ") = rng <:(pr2 (X,Y)),(pr1 (X,Y)):> by FUNCT_1:32
.= [:Y,X:] by Th4 ;

A2: now :: thesis: for x being object st x in [:Y,X:] holds
(<:(pr2 (X,Y)),(pr1 (X,Y)):> ") . x = <:(pr2 (Y,X)),(pr1 (Y,X)):> . x

let x be object ; :: thesis: ( x in [:Y,X:] implies (<:(pr2 (X,Y)),(pr1 (X,Y)):> ") . x = <:(pr2 (Y,X)),(pr1 (Y,X)):> . x )
assume x in [:Y,X:] ; :: thesis: (<:(pr2 (X,Y)),(pr1 (X,Y)):> ") . x = <:(pr2 (Y,X)),(pr1 (Y,X)):> . x
then consider x1, x2 being object such that
A3: ( x1 in Y & x2 in X ) and
A4: x = [x1,x2] by ZFMISC_1:def 2;
A5: ( <:(pr2 (Y,X)),(pr1 (Y,X)):> . (x1,x2) = [x2,x1] & <:(pr2 (X,Y)),(pr1 (X,Y)):> . (x2,x1) = [x1,x2] ) by A3, Lm1;
dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:X,Y:] by Th4;
then [x2,x1] in dom <:(pr2 (X,Y)),(pr1 (X,Y)):> by A3, ZFMISC_1:87;
hence (<:(pr2 (X,Y)),(pr1 (X,Y)):> ") . x = <:(pr2 (Y,X)),(pr1 (Y,X)):> . x by A4, A5, FUNCT_1:32; :: thesis: verum

end;

dom <:(pr2 (Y,X)),(pr1 (Y,X)):> = [:Y,X:] by Th4;
hence <:(pr2 (X,Y)),(pr1 (X,Y)):> " = <:(pr2 (Y,X)),(pr1 (Y,X)):> by A1, A2; :: thesis: verum