:: deftheorem defines is_applicable_to ABCMIZ_0:def 21 :
for T being non empty reflexive transitive non void TA-structure
for t being type of T
for v being FinSequence of the adjectives of T holds
( v is_applicable_to t iff for i being Nat
for a being adjective of T
for s being type of T st i in dom v & a = v . i & s = (apply (v,t)) . i holds
a is_applicable_to s );