for Q being multLoop
for N being SubLoop of Q
for f being Function of Q,Q st f in Mlt (@ ([#] N)) holds
for x being Element of Q holds
( x in @ ([#] N) iff f . x in @ ([#] N) )