theorem :: RELSET_2:64

for A, B being set
for R being Relation of A,B holds (id A) * R = R * (id B)