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:57;
apply (<*a*>,t) = <*t,(a ast t)*> by Th30;
hence <*a*> ast t = a ast t by A1, FINSEQ_1:61; :: thesis: verum