let X, Y be set ; :: thesis: ( dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:X,Y:] & rng <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:Y,X:] )
set f = <:(pr2 (X,Y)),(pr1 (X,Y)):>;
thus A1: dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = (dom (pr2 (X,Y))) /\ (dom (pr1 (X,Y))) by FUNCT_3:def 7
.= (dom (pr2 (X,Y))) /\ [:X,Y:] by FUNCT_3:def 4
.= [:X,Y:] /\ [:X,Y:] by FUNCT_3:def 5
.= [:X,Y:] ; :: thesis: rng <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:Y,X:]
rng <:(pr2 (X,Y)),(pr1 (X,Y)):> c= [:(rng (pr2 (X,Y))),(rng (pr1 (X,Y))):] by FUNCT_3:51;
hence rng <:(pr2 (X,Y)),(pr1 (X,Y)):> c= [:Y,X:] by XBOOLE_1:1; :: according to XBOOLE_0:def 10 :: thesis: [:Y,X:] c= rng <:(pr2 (X,Y)),(pr1 (X,Y)):>
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [:Y,X:] or y in rng <:(pr2 (X,Y)),(pr1 (X,Y)):> )
assume y in [:Y,X:] ; :: thesis: y in rng <:(pr2 (X,Y)),(pr1 (X,Y)):>
then consider y1, y2 being object such that
A2: ( y1 in Y & y2 in X ) and
A3: y = [y1,y2] by ZFMISC_1:def 2;
A4: [y2,y1] in dom <:(pr2 (X,Y)),(pr1 (X,Y)):> by A1, A2, ZFMISC_1:87;
<:(pr2 (X,Y)),(pr1 (X,Y)):> . (y2,y1) = y by A2, A3, Lm1;
hence y in rng <:(pr2 (X,Y)),(pr1 (X,Y)):> by A4, FUNCT_1:def 3; :: thesis: verum