theorem :: FUNCT_3:69

for X, Y being set holds [:(id X),(id Y):] = id [:X,Y:]