let X, Y be set ; [:(id X),(id Y):] = id [:X,Y:]
rng (pr1 (X,Y)) c= X
by Th59;
then A1:
(id X) * (pr1 (X,Y)) = pr1 (X,Y)
by RELAT_1:79;
rng (pr2 (X,Y)) c= Y
by Th61;
then A2:
(id Y) * (pr2 (X,Y)) = pr2 (X,Y)
by RELAT_1:79;
( dom (id X) = X & dom (id Y) = Y )
by RELAT_1:71;
hence [:(id X),(id Y):] =
<:(pr1 (X,Y)),(pr2 (X,Y)):>
by A1, A2, Th87
.=
id [:X,Y:]
by Th73
;
verum