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