let X, Y be set ; :: thesis: <:(pr1 X,Y),(pr2 X,Y):> = id [:X,Y:]
( dom (pr1 X,Y) = [:X,Y:] & dom (pr2 X,Y) = [:X,Y:] ) by Def5, Def6;
then A1: dom <:(pr1 X,Y),(pr2 X,Y):> = [:X,Y:] by Th70;
A2: for x, y being set st x in X & y in Y holds
<:(pr1 X,Y),(pr2 X,Y):> . x,y = (id [:X,Y:]) . x,y

proof

let x, y be set ; :: thesis: ( x in X & y in Y implies <:(pr1 X,Y),(pr2 X,Y):> . x,y = (id [:X,Y:]) . x,y )
assume A3: ( x in X & y in Y ) ; :: thesis: <:(pr1 X,Y),(pr2 X,Y):> . x,y = (id [:X,Y:]) . x,y
then A4: [x,y] in [:X,Y:] by ZFMISC_1:106;
hence <:(pr1 X,Y),(pr2 X,Y):> . x,y = [((pr1 X,Y) . x,y),((pr2 X,Y) . x,y)] by A1, Def8
.= [x,((pr2 X,Y) . x,y)] by A3, Def5
.= [x,y] by A3, Def6
.= (id [:X,Y:]) . x,y by A4, FUNCT_1:35 ;
:: thesis: verum

end;

dom (id [:X,Y:]) = [:X,Y:] by RELAT_1:71;
hence <:(pr1 X,Y),(pr2 X,Y):> = id [:X,Y:] by A1, A2, Th6; :: thesis: verum