let T be non empty reflexive transitive non void TA-structure ; :: thesis: for t being type of T
for v1, v2 being FinSequence of the adjectives of T holds (apply (v1 ^ v2),t) . ((len v1) + 1) = v1 ast t
let t be type of T; :: thesis: for v1, v2 being FinSequence of the adjectives of T holds (apply (v1 ^ v2),t) . ((len v1) + 1) = v1 ast t
let v1, v2 be FinSequence of the adjectives of T; :: thesis: (apply (v1 ^ v2),t) . ((len v1) + 1) = v1 ast t
set v = v1 ^ v2;
A1: len (apply v2,(v1 ast t)) = (len v2) + 1 by Def19;
A2: apply (v1 ^ v2),t = (apply v1,t) $^ (apply v2,(v1 ast t)) by Th35;
len (apply v1,t) = (len v1) + 1 by Def19;
then (apply (v1 ^ v2),t) . (((len v1) + 1) + 0 ) = (apply v2,(v1 ast t)) . (0 + 1) by A1, A2, Th34;
hence (apply (v1 ^ v2),t) . ((len v1) + 1) = v1 ast t by Def19; :: thesis: verum