:: deftheorem Def19 defines apply ABCMIZ_0:def 19 :
for T being non empty reflexive transitive non void TA-structure
for t being type of T
for p being FinSequence of the adjectives of T
for b₄ being FinSequence of the carrier of T holds
( b₄ = apply (p,t) iff ( len b₄ = (len p) + 1 & b₄ . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = b₄ . i holds
b₄ . (i + 1) = a ast t ) ) );