theorem Th35: :: ABCMIZ_0:35

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
for i being Nat st i in dom v1 holds
(apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i