let T be non empty reflexive transitive non void TA-structure ; :: thesis: for t being type of T holds apply (<*> the adjectives of T),t = <*t*>
let t be type of T; :: thesis: apply (<*> the adjectives of T),t = <*t*>
( len (apply (<*> the adjectives of T),t) = 0 + 1 & (apply (<*> the adjectives of T),t) . 1 = t ) by Def19, CARD_1:47;
hence apply (<*> the adjectives of T),t = <*t*> by FINSEQ_1:57; :: thesis: verum