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