let X, Y be set ; <:(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 for x being object st x in [:Y,X:] holds
(<:(pr2 (X,Y)),(pr1 (X,Y)):> ") . x = <:(pr2 (Y,X)),(pr1 (Y,X)):> . xlet x be
object ;
( x in [:Y,X:] implies (<:(pr2 (X,Y)),(pr1 (X,Y)):> ") . x = <:(pr2 (Y,X)),(pr1 (Y,X)):> . x )assume
x in [:Y,X:]
;
(<:(pr2 (X,Y)),(pr1 (X,Y)):> ") . x = <:(pr2 (Y,X)),(pr1 (Y,X)):> . xthen 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;
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; verum