theorem Th37: :: ABCMIZ_0:37

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 v2 ast (v1 ast t) = (v1 ^ v2) ast t