theorem Th29: :: ABCMIZ_0:29

for T being non empty reflexive transitive non void TA-structure
for t being type of T
for a being adjective of T holds apply (<*a*>,t) = <*t,(a ast t)*>