theorem Th36: :: ABCMIZ_0:36

for T being non empty reflexive transitive non void TA-structure
for t being type of T
for v1, v2 being FinSequence of the adjectives of T holds (apply ((v1 ^ v2),t)) . ((len v1) + 1) = v1 ast t