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 apply <*a*>,t = <*t,(a ast t)*>
let t be type of T; :: thesis: for a being adjective of T holds apply <*a*>,t = <*t,(a ast t)*>
let a be adjective of T; :: thesis: apply <*a*>,t = <*t,(a ast t)*>
A1: len <*a*> = 1 by FINSEQ_1:57;
then A2: ( len (apply <*a*>,t) = 1 + 1 & (apply <*a*>,t) . 1 = t & <*a*> . 1 = a & 1 in dom <*a*> ) by Def19, FINSEQ_1:57, FINSEQ_3:27;
then (apply <*a*>,t) . ((len <*a*>) + 1) = a ast t by A1, Def19;
hence apply <*a*>,t = <*t,(a ast t)*> by A1, A2, FINSEQ_1:61; :: thesis: verum