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*>
A1: (apply ((<*> the adjectives of T),t)) . 1 = t by Def19;
len (apply ((<*> the adjectives of T),t)) = 0 + 1 by Def19, CARD_1:27;
hence apply ((<*> the adjectives of T),t) = <*t*> by A1, FINSEQ_1:40; :: thesis: verum