theorem Th61: :: AIMLOOP:64

for Q being multLoop
for x, y being Element of Q holds
( x * (lp (Nucl Q)) = y * (lp (Nucl Q)) iff ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) )