for Q being AIM multLoop
for x, u being Element of Q st u in Nucl Q holds
T_map (u,x) in Nucl Q