:: deftheorem defines satisfying_RR AIMLOOP:def 12 :
for Q being multLoop holds
( Q is satisfying_RR iff for u, x, y, z, w being Element of Q holds R_map ((R_map (u,x,y)),z,w) = R_map ((R_map (u,z,w)),x,y) );