let T be non empty reflexive transitive non void TA-structure ; 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; 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; v2 ast (v1 ast t) = (v1 ^ v2) ast t
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;
A2:
len (apply (v1,t)) = (len v1) + 1
by Def19;
len <*q*> = 1
by FINSEQ_1:39;
then A3:
(len v1) + 1 = (len tt) + 1
by A2, A1, FINSEQ_1:22;
A4:
(len v2) + 1 >= 1
by NAT_1:11;
len (apply (v2,(v1 ast t))) = (len v2) + 1
by Def19;
then A5:
(len v2) + 1 in dom (apply (v2,(v1 ast t)))
by A4, FINSEQ_3:25;
apply ((v1 ^ v2),t) =
(apply (v1,t)) $^ (apply (v2,(v1 ast t)))
by Th35
.=
tt ^ (apply (v2,(v1 ast t)))
by A1, REWRITE1:2
;
hence v2 ast (v1 ast t) =
(apply ((v1 ^ v2),t)) . ((len tt) + ((len v2) + 1))
by A5, FINSEQ_1:def 7
.=
(apply ((v1 ^ v2),t)) . (((len v1) + (len v2)) + 1)
by A3
.=
(v1 ^ v2) ast t
by FINSEQ_1:22
;
verum