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