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
for i being Nat st i in dom v1 holds
(apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i
let t be type of T; :: thesis: for v1, v2 being FinSequence of the adjectives of T
for i being Nat st i in dom v1 holds
(apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i
let v1, v2 be FinSequence of the adjectives of T; :: thesis: for i being Nat st i in dom v1 holds
(apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i
set v = v1 ^ v2;
consider tt being FinSequence of the carrier of T, q being Element of T such that
A1: apply (v1,t) = tt ^ <*q*> by HILBERT2:4;
let i be Nat; :: thesis: ( i in dom v1 implies (apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i )
A2: len (apply (v1,t)) = (len v1) + 1 by Def19;
assume A3: i in dom v1 ; :: thesis: (apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i
then A4: i >= 1 by FINSEQ_3:25;
len <*q*> = 1 by FINSEQ_1:39;
then (len v1) + 1 = (len tt) + 1 by A2, A1, FINSEQ_1:22;
then i <= len tt by A3, FINSEQ_3:25;
then A5: i in dom tt by A4, FINSEQ_3:25;
apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t))) by Th34
.= tt ^ (apply (v2,(v1 ast t))) by A1, REWRITE1:2 ;
then (apply ((v1 ^ v2),t)) . i = tt . i by A5, FINSEQ_1:def 7;
hence (apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i by A1, A5, FINSEQ_1:def 7; :: thesis: verum