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 Y,X),(pr1 Y,X):> = [:Y,X:] by Th4;
A2: dom (<:(pr2 X,Y),(pr1 X,Y):> " ) = rng <:(pr2 X,Y),(pr1 X,Y):> by FUNCT_1:54
.= [:Y,X:] by Th4 ;

now

let x be set ; :: 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 set such that
A3: ( x1 in Y & x2 in X & x = [x1,x2] ) by ZFMISC_1:def 2;
A4: <:(pr2 Y,X),(pr1 Y,X):> . x1,x2 = [x2,x1] by A3, Lm1;
dom <:(pr2 X,Y),(pr1 X,Y):> = [:X,Y:] by Th4;
then A5: [x2,x1] in dom <:(pr2 X,Y),(pr1 X,Y):> by A3, ZFMISC_1:106;
<:(pr2 X,Y),(pr1 X,Y):> . x2,x1 = [x1,x2] by A3, Lm1;
hence (<:(pr2 X,Y),(pr1 X,Y):> " ) . x = <:(pr2 Y,X),(pr1 Y,X):> . x by A3, A4, A5, FUNCT_1:54; :: thesis: verum

end;

hence <:(pr2 X,Y),(pr1 X,Y):> " = <:(pr2 Y,X),(pr1 Y,X):> by A1, A2, FUNCT_1:9; :: thesis: verum