:: deftheorem Def28a defines unity-preserving AIMLOOP:def 28 :
for Q1, Q2 being multLoop
for f being Function of Q1,Q2 holds
( f is unity-preserving iff f . (1. Q1) = 1. Q2 );