theorem Th58: :: AIMLOOP:61

for Q being multLoop
for x, y being Element of Q holds R_MAP (x,y) in InnAut Q