let X, Y be set ; :: thesis: <:(pr2 X,Y),(pr1 X,Y):> is one-to-one
set f = <:(pr2 X,Y),(pr1 X,Y):>;
let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in proj1 <:(pr2 X,Y),(pr1 X,Y):> or not y in proj1 <:(pr2 X,Y),(pr1 X,Y):> or not <:(pr2 X,Y),(pr1 X,Y):> . x = <:(pr2 X,Y),(pr1 X,Y):> . y or x = y )
assume that
A1: x in dom <:(pr2 X,Y),(pr1 X,Y):> and
A2: y in dom <:(pr2 X,Y),(pr1 X,Y):> and
A3: <:(pr2 X,Y),(pr1 X,Y):> . x = <:(pr2 X,Y),(pr1 X,Y):> . y ; :: thesis: x = y
A4: dom <:(pr2 X,Y),(pr1 X,Y):> = [:X,Y:] by Th4;
then consider x1, x2 being set such that
A5: ( x1 in X & x2 in Y ) and
A6: x = [x1,x2] by A1, ZFMISC_1:def 2;
consider y1, y2 being set such that
A7: ( y1 in X & y2 in Y ) and
A8: y = [y1,y2] by A4, A2, ZFMISC_1:def 2;
A9: <:(pr2 X,Y),(pr1 X,Y):> . y1,y2 = [y2,y1] by A7, Lm1;
A10: <:(pr2 X,Y),(pr1 X,Y):> . x1,x2 = [x2,x1] by A5, Lm1;
then x1 = y1 by A3, A6, A8, A9, ZFMISC_1:33;
hence x = y by A3, A6, A8, A10, A9, ZFMISC_1:33; :: thesis: verum