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 8
.= (dom (pr2 X,Y)) /\ [:X,Y:] by FUNCT_3:def 5
.= [:X,Y:] /\ [:X,Y:] by FUNCT_3:def 6
.= [: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:71;
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 set ; :: 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 set 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:106;
<:(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 5; :: thesis: verum