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:54
.= [:Y,X:] by Th4 ;

A2: 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 ) 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:106;
hence (<:(pr2 X,Y),(pr1 X,Y):> " ) . x = <:(pr2 Y,X),(pr1 Y,X):> . x by A4, A5, FUNCT_1:54; :: 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, FUNCT_1:9; :: thesis: verum