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 Def4, Def5;
then A1: dom <:(pr1 (X,Y)),(pr2 (X,Y)):> = [:X,Y:] by Th50;
A2: for x, y being object 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 object ; :: 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:87;
hence <:(pr1 (X,Y)),(pr2 (X,Y)):> . (x,y) = [((pr1 (X,Y)) . (x,y)),((pr2 (X,Y)) . (x,y))] by A1, Def7
.= [x,((pr2 (X,Y)) . (x,y))] by A3, Def4
.= [x,y] by A3, Def5
.= (id [:X,Y:]) . (x,y) by A4, FUNCT_1:18 ;
:: thesis: verum

end;

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