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