theorem Th22: :: SCMRING2:22

for R being Ring holds Data-Locations = Data-Locations