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