:: deftheorem Def19 defines satisfying_aK1 AIMLOOP:def 19 :
for Q being multLoop holds
( Q is satisfying_aK1 iff for x, y, z, u being Element of Q holds a_op ((K_op (x,y)),z,u) = 1. Q );