theorem Th16: :: TOPGRP_1:17

for H being non empty multMagma
for P being Subset of H
for h being Element of H holds (* h) .: P = P * h