theorem :: AIMLOOP:11

for Q being multLoop
for x, y, z being Element of Q st a_op (x,y,z) = 1. Q holds
L_map (z,y,x) = z