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: <*a*> . 1 = a by FINSEQ_1:57;
A2: (apply <*a*>,t) . 1 = t by Def19;
A3: len <*a*> = 1 by FINSEQ_1:57;
then A4: len (apply <*a*>,t) = 1 + 1 by Def19;
1 in dom <*a*> by A3, FINSEQ_3:27;
then (apply <*a*>,t) . ((len <*a*>) + 1) = a ast t by A3, A2, A1, Def19;
hence apply <*a*>,t = <*t,(a ast t)*> by A3, A4, A2, FINSEQ_1:61; :: thesis: verum