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