:: deftheorem TM1 defines T_MAP AIMLOOP:def 53 :
for Q being multLoop
for x being Element of Q
for b₃ being Function of Q,Q holds
( b₃ = T_MAP x iff for u being Element of Q holds b₃ . u = T_map (u,x) );