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 st v1 ^ v2 is_applicable_to t holds
( v1 is_applicable_to t & v2 is_applicable_to v1 ast t )
let t be type of T; :: thesis: for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_applicable_to t holds
( v1 is_applicable_to t & v2 is_applicable_to v1 ast t )
let v1, v2 be FinSequence of the adjectives of T; :: thesis: ( v1 ^ v2 is_applicable_to t implies ( v1 is_applicable_to t & v2 is_applicable_to v1 ast t ) )
set v = v1 ^ v2;
A1: apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t))) by Th34;
A2: len (apply (v2,(v1 ast t))) = (len v2) + 1 by Def19;
assume A3: for i being Nat
for a being adjective of T
for s being type of T st i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & s = (apply ((v1 ^ v2),t)) . i holds
a is_applicable_to s ; :: according to ABCMIZ_0:def 21 :: thesis: ( v1 is_applicable_to t & v2 is_applicable_to v1 ast t )

hereby :: according to ABCMIZ_0:def 21 :: thesis: v2 is_applicable_to v1 ast t

A4: dom v1 c= dom (v1 ^ v2) by FINSEQ_1:26;
let i be Nat; :: thesis: for a being adjective of T
for s being type of T st i in dom v1 & a = v1 . i & s = (apply (v1,t)) . i holds
a is_applicable_to s
let a be adjective of T; :: thesis: for s being type of T st i in dom v1 & a = v1 . i & s = (apply (v1,t)) . i holds
a is_applicable_to s
let s be type of T; :: thesis: ( i in dom v1 & a = v1 . i & s = (apply (v1,t)) . i implies a is_applicable_to s )
assume that
A5: i in dom v1 and
A6: a = v1 . i and
A7: s = (apply (v1,t)) . i ; :: thesis: a is_applicable_to s
A8: a = (v1 ^ v2) . i by A5, A6, FINSEQ_1:def 7;
s = (apply ((v1 ^ v2),t)) . i by A5, A7, Th35;
hence a is_applicable_to s by A3, A5, A4, A8; :: thesis: verum

end;

let i be Nat; :: according to ABCMIZ_0:def 21 :: thesis: for a being adjective of T
for s being type of T st i in dom v2 & a = v2 . i & s = (apply (v2,(v1 ast t))) . i holds
a is_applicable_to s
let a be adjective of T; :: thesis: for s being type of T st i in dom v2 & a = v2 . i & s = (apply (v2,(v1 ast t))) . i holds
a is_applicable_to s
let s be type of T; :: thesis: ( i in dom v2 & a = v2 . i & s = (apply (v2,(v1 ast t))) . i implies a is_applicable_to s )
assume that
A9: i in dom v2 and
A10: a = v2 . i and
A11: s = (apply (v2,(v1 ast t))) . i ; :: thesis: a is_applicable_to s
A12: a = (v1 ^ v2) . ((len v1) + i) by A9, A10, FINSEQ_1:def 7;
i >= 1 by A9, FINSEQ_3:25;
then consider j being Nat such that
A13: i = 1 + j by NAT_1:10;
i <= len v2 by A9, FINSEQ_3:25;
then j < len v2 by A13, NAT_1:13;
then A14: j < len (apply (v2,(v1 ast t))) by A2, NAT_1:13;
len (apply (v1,t)) = (len v1) + 1 by Def19;
then (len v1) + i = (len (apply (v1,t))) + j by A13;
then s = (apply ((v1 ^ v2),t)) . ((len v1) + i) by A11, A1, A13, A14, Th33;
hence a is_applicable_to s by A3, A9, A12, FINSEQ_1:28; :: thesis: verum