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 v2 ast (v1 ast t) = (v1 ^ v2) ast t
let t be type of T; :: thesis: for v1, v2 being FinSequence of the adjectives of T holds v2 ast (v1 ast t) = (v1 ^ v2) ast t
let v1, v2 be FinSequence of the adjectives of T; :: thesis: v2 ast (v1 ast t) = (v1 ^ v2) ast t
set v = v1 ^ v2;
A1: ( len (apply v1,t) = (len v1) + 1 & len (apply v2,(v1 ast t)) = (len v2) + 1 ) by Def19;
consider tt being FinSequence of the carrier of T, q being Element of T such that
A2: apply v1,t = tt ^ <*q*> by HILBERT2:4;
A3: apply (v1 ^ v2),t = (apply v1,t) $^ (apply v2,(v1 ast t)) by Th35
.= tt ^ (apply v2,(v1 ast t)) by A2, REWRITE1:2 ;
( len (apply v2,(v1 ast t)) = (len v2) + 1 & (len v2) + 1 >= 1 ) by Def19, NAT_1:11;
then A4: (len v2) + 1 in dom (apply v2,(v1 ast t)) by FINSEQ_3:27;
len <*q*> = 1 by FINSEQ_1:56;
then A5: (len v1) + 1 = (len tt) + 1 by A1, A2, FINSEQ_1:35;
thus v2 ast (v1 ast t) = (apply (v1 ^ v2),t) . ((len tt) + ((len v2) + 1)) by A3, A4, FINSEQ_1:def 7
.= (apply (v1 ^ v2),t) . (((len v1) + (len v2)) + 1) by A5
.= (v1 ^ v2) ast t by FINSEQ_1:35 ; :: thesis: verum