let T be non empty reflexive transitive non void TA-structure ; :: thesis: for t being type of T
for a being adjective of T holds <*a*> ast t = a ast t
let t be type of T; :: thesis: for a being adjective of T holds <*a*> ast t = a ast t
let a be adjective of T; :: thesis: <*a*> ast t = a ast t
A1: len <*a*> = 1 by FINSEQ_1:40;
apply (<*a*>,t) = <*t,(a ast t)*> by Th29;
hence <*a*> ast t = a ast t by A1; :: thesis: verum