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 ;
A2: (apply (<*a*>,t)) . 1 = t by Def19;
A3: len <*a*> = 1 by FINSEQ_1:40;
then A4: len (apply (<*a*>,t)) = 1 + 1 by Def19;
1 in dom <*a*> by A3, FINSEQ_3:25;
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:44; :: thesis: verum