:: deftheorem Def9 defines compositional ALTCAT_1:def 9 :
for IT being Function holds
( IT is compositional iff for x being object st x in dom IT holds
ex f, g being Function st
( x = [g,f] & IT . x = g * f ) );