let X, Y be set ; [:(id X),(id Y):] = id [:X,Y:]
rng (pr1 (X,Y)) c= X
by Th43;
then A1:
(id X) * (pr1 (X,Y)) = pr1 (X,Y)
by RELAT_1:53;
rng (pr2 (X,Y)) c= Y
by Th45;
then A2:
(id Y) * (pr2 (X,Y)) = pr2 (X,Y)
by RELAT_1:53;
( dom (id X) = X & dom (id Y) = Y )
;
hence [:(id X),(id Y):] =
<:(pr1 (X,Y)),(pr2 (X,Y)):>
by A1, A2, Th66
.=
id [:X,Y:]
by Th53
;
verum